Faster and more complete extended static checking for the Java modeling language

DOI10.1007/s10817-009-9134-9zbMath1185.68143OpenAlexW2015771391MaRDI QIDQ2655328

Perry R. James, Patrice Chalin

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9134-9

zbMATH Keywords

static verificationtheorem proversESCESC4extended static checkingJava Modeling LanguageJML4

Mathematics Subject Classification ID

Related Items (2)

Heaps and Data Structures: A Challenge for Automated Provers ⋮ ESC4

Uses Software

• HOL-Boogie
• Isabelle
• Why3
• Metis_
• Spec#
• Isar
• Omnibus
• distcc
• MetaPRL
• Caduceus
• ESC/Java
• Boogie
• JACK

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Avoiding exponential explosion
• Unnamed Item
• Unnamed Item

This page was built for publication: Faster and more complete extended static checking for the Java modeling language