jahob

KO | EN

gitlite — search

#react #ai #golang #android #machine-learning #rust #deep-learning #linux #windows #awesome #vue #security #ios #openai

(★ 12)

Jahob Verification System

jahob Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

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

jahob

jahob Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

jahob

jahob Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README