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

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

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

Uses Software

• Why3
• Metis_
• Spec#
• Isar
• Omnibus
• distcc
• MetaPRL
• Caduceus
• ESC/Java
• Boogie
• JACK
• Unnamed Item
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• 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

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