[Why3-club] Failed Why3 Project?

s-dnovik s-dnovik at haw-landshut.de
Wed Jan 30 12:20:30 CET 2019


Looking at SPARK/Ada, I learned about the Why3 platform. It seemed 
interesting to me and I wanted to try it out.

So I wrote a Bachelor's Thesis about Verification of MIPS Assembly with 
Why3:  https://github.com/zul2/mips2why3

The aim was to explain Why3 to students and give them the opportunity to 
verify simple MIPS programs.

I liked my work (especially the MIPS instruction set model worked fine).

Unfortunately the Prof said the work is all bad (without giving much 

Would you say, that I messed it up working with your tool?

If yes, I would apologize for my ignorance and remove the repository 
again ;)

Best Regards,


More information about the Why3-club mailing list