Weakest pre-condition reasoning for Java programs with JML annotations

DOI10.1016/J.JLAP.2003.07.005MaRDI QIDQ1881666zbMATH OpenOpenAlexFDO

Authors Bart Jacobs

Publication date 14 October 2004

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2003.07.005

zbMATH Keywords

JavaProgram correctnessWeakest preconditionProgram logics

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Weakest Preconditions for High-Level Programs
• scientific article; zbMATH DE number 1487496
• Weakest preconditions for pure Prolog programs
• Instrumenting a weakest precondition calculus for counterexample generation
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• scientific article; zbMATH DE number 4047056
• Weakest relative precondition semantics. Balancing approved theory and realistic translation verification
• scientific article; zbMATH DE number 1927431
• scientific article; zbMATH DE number 1796120

Cites work

• scientific article; zbMATH DE number 1617288 (Why is no real title available?)
• scientific article; zbMATH DE number 1629956 (Why is no real title available?)
• scientific article; zbMATH DE number 1692946 (Why is no real title available?)
• scientific article; zbMATH DE number 1693527 (Why is no real title available?)
• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 1706337 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 1848384 (Why is no real title available?)
• scientific article; zbMATH DE number 1860624 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A case study in class library verification: Java's vector class
• Programming as a Discipline of Mathematical Nature
• Source code verification of a secure payment applet
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML

Cited in

(11)

• WP semantics and behavioral subtyping
• Efficient weakest preconditions
• scientific article; zbMATH DE number 1949610 (Why is no real title available?)
• Verification of object-oriented programs: a transformational approach
• scientific article; zbMATH DE number 1693527 (Why is no real title available?)
• Verification conditions for source-level imperative programs
• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Specification and verification challenges for sequential object-oriented programs
• A proof outline logic for object-oriented programming
• Verifying and generating WP transformers for procedures on complex data

Describes a project that uses

Uses Software

• LOOP
• ESC/Java
• HOL
• JML
• PVS
• KRAKATOA

This page was built for publication: Weakest pre-condition reasoning for Java programs with JML annotations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1881666)