Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
jahob_system [2011/02/09 20:51] vkuncak |
jahob_system [2017/03/19 16:33] vkuncak |
||
---|---|---|---|
Line 2: | Line 2: | ||
Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints. | Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints. | ||
+ | |||
+ | **Jahob is now on github:** | ||
+ | https://github.com/epfl-lara/jahob | ||
+ | |||
+ | Note | ||
+ | * Information below may be outdated | ||
+ | * Java may be outdated. Consider Scala, http://www.scala-lang.org/ | ||
+ | * To verify Scala, consider tools such as http://leon.epfl.ch and its successors | ||
+ | |||
+ | ---- | ||
[[data_structure_examples.html|Some of the data structures verified in Jahob]] | [[data_structure_examples.html|Some of the data structures verified in Jahob]] | ||
Line 68: | Line 78: | ||
Some relevant publications: | Some relevant publications: | ||
- | * [[http://pub.ist.ac.at/~wies/papers/CounterexampleGuidedFocus.pdf|Andreas Podelski, Thomas Wies: Counterexample-Guided Focus]] | + | * [[http://pub.ist.ac.at/~wies/papers/CounterexampleGuidedFocus.pdf|Andreas Podelski, Thomas Wies: Counterexample-Guided Focus (POPL), 2010.]] |
* [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL09IntegratedProofLanguageforImperativePrograms.html|Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In ACM Conf. Programming Language Design and Implementation (PLDI), 2009.]] | * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL09IntegratedProofLanguageforImperativePrograms.html|Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In ACM Conf. Programming Language Design and Implementation (PLDI), 2009.]] | ||
* [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In ACM Conf. Programming Language Design and Implementation (PLDI), 2008.]] | * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In ACM Conf. Programming Language Design and Implementation (PLDI), 2008.]] | ||
Line 85: | Line 95: | ||
Jahob project is supported by the funding from the US and Swiss National Science Foundations. | Jahob project is supported by the funding from the US and Swiss National Science Foundations. | ||
- | Here is a [[http://cag.csail.mit.edu/~vkuncak/projects/jahob/index.html |previous Jahob page]]. |