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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)
- Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
- Lynch, Christopher; Ranise, Silvio; Ringeissen, Christophe; Tran, Duc-Khanh: Automatic decidability and combinability (2011)
- Bonacina, Maria Paola; Echenim, Mnacho: Theory decision by decomposition (2010)
- Kreiker, Jörg; Seidl, Helmut; Vojdani, Vesal: Shape analysis of low-level C with overlapping structures (2010)
- Meng, Jia; Paulson, Lawrence C.: Translating higher-order clauses to first-order clauses (2008)
- Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin: Using first-order theorem provers in the Jahob data structure verification system (2007)
- Kuncak, Viktor; Rinard, Martin: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic (2007)
- Sevcík, Jaroslav: Proving resource consumption of low-level programs using automated theorem provers. (2007)