Dafny – A programming language with a program verifier

Re:Dafny – A programming language with a program verifier by tom_mellior on Friday January 20, 2017 @04:38AM (#13442602)

> I also recall some Java extension but can't find it atm.

You might be thinking of JML (Java Modeling Language): http://www.eecs.ucf.edu/~leavens/JML//index.shtml Apparently JML-annotated programs can passed to Why3 using a confusingly documented set of tools: http://krakatoa.lri.fr/

There is also the Cheker Framework for Java: http://types.cs.washington.edu/checker-framework/ But as far as I understand it's less general than all the other tools you mention.

[ Parent | on HN ]

Re:Dafny – A programming language with a program verifier by tom_mellior on Friday January 20, 2017 @06:52AM (#13443147)

Also, and probably even more likely than the ones I mentioned above, there is KeY for Java verification: http://www.key-project.org/index.php

[ Parent | on HN ]