Skip to content

Jahob Verification System

License

GPL-2.0, Unknown licenses found

Licenses found

GPL-2.0
COPYING.GPL
Unknown
COPYING.MIT
Notifications You must be signed in to change notification settings

epfl-lara/jahob

Repository files navigation

JAHOB VERIFICATION SYSTEM

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.

A partial list of some relevant publications:

  • Andreas Podelski, Thomas Wies: Counterexample-Guided Focus (POPL), 2010.
  • Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In ACM Conf. Programming Language Design and Implementation (PLDI), 2009.
  • Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In ACM Conf. Programming Language Design and Implementation (PLDI), 2008.
  • Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard. Using first-order theorem provers in the Jahob data structure verification system. In Verification, * Model Checking and Abstract Interpretation, volume 4349 of LNCS, November 2007.
  • Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard. Field constraint analysis. In Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation, volume 3855 of LNCS, 2006.
  • Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard. Verifying complex properties using symbolic shape analysis. In Workshop on Heap Abstraction and Verification (collocated with ETAPS), 2007.
  • Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In 20th International Conference on Automated Deduction, CADE-20, volume 3632 of LNCS, Tallinn, Estonia, July 2005.

PhD Theses (chronological):

About

Jahob Verification System

Topics

Resources

License

GPL-2.0, Unknown licenses found

Licenses found

GPL-2.0
COPYING.GPL
Unknown
COPYING.MIT

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published