[Why3-club] Failed Why3 Project?

Yannick Moy moy at adacore.com
Wed Jan 30 14:00:41 CET 2019


Hi Dmitrij,

I looked at your report (https://github.com/zul2/mips2why3/blob/master/bachelors_thesis/main.pdf <https://github.com/zul2/mips2why3/blob/master/bachelors_thesis/main.pdf>) and found it clear and interesting. You seem to have understood well how deductive verification tools like SPARK or Why3 work, and you have used Why3 in a reasonable way to provide deductive verification of MIPS assembly. I found your presentation pedagogical, so it could be useful for others who discover this field.

Recent exciting work is using similarly SMT provers on assembly code, see Alive (http://web.ist.utl.pt/nuno.lopes/pubs/alive-cacm18.pdf <http://web.ist.utl.pt/nuno.lopes/pubs/alive-cacm18.pdf> and https://www.rise4fun.com/Alive <https://www.rise4fun.com/Alive>).
Or this work on using SPARK for proving the security of binary code: https://blog.adacore.com/research-corner-proving-security-of-binary-programs-with-spark <https://blog.adacore.com/research-corner-proving-security-of-binary-programs-with-spark>

I cannot comment on the assessment of your professor, I suggest you discuss with him/her the rationale for his assessment?

Hope that helps
--
Yannick Moy, Senior Software Engineer, AdaCore


-- s-dnovik (2019-01-30)
> Hello,
> 
> 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 <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 detail).
> 
> 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,
> 
> Dmitrij
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr <mailto:Why3-club at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190130/e3ebc308/attachment.html>


More information about the Why3-club mailing list