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):

• Viktor Kuncak (2007): Modular Data Structure Verification, https://dspace.mit.edu/handle/1721.1/38533
• Thomas Wies (2009): Symbolic Shape Analysis, http://cs.nyu.edu/wies/publ/wies09phdthesis.pdf
• Karen Zee (2010): Verification of full functional correctness for imperative linked data structures, https://dspace.mit.edu/handle/1721.1/58078