Efficient weakest preconditions

DOI10.1016/J.IPL.2004.10.015MaRDI QIDQ835051zbMATH OpenOpenAlexFDO

Authors K. Rustan M. Leino

Publication date 27 August 2009

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2004.10.015

zbMATH Keywords

automatic theorem provingformal semanticsprogram correctness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Weakest pre-condition reasoning for Java programs with JML annotations
• scientific article; zbMATH DE number 3917681
• Verification conditions for source-level imperative programs
• Weakest Preconditions for High-Level Programs
• Computing Preconditions and Postconditions of While Loops

Cites work

• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Avoiding exponential explosion: generating compact verification conditions
• Combining angels, demons and miracles in program specifications
• Correct and Robust Programs
• Programming as a Discipline of Mathematical Nature
• Simplify: a theorem prover for program checking

Cited in

(16)

• On the weak prefix-search problem
• Verifying Whiley programs with Boogie
• Weakest invariant generation for automated addition of fault-tolerance
• Function extraction
• Horn clause solvers for program verification
• Instrumenting a weakest precondition calculus for counterexample generation
• Backward symbolic execution with loop folding
• Knowledge forgetting in propositional \(\mu\)-calculus
• Verification conditions for source-level imperative programs
• Doomed program points
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Improving Generalization in Software IC3
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Quantitative information flow as safety and liveness hyperproperties
• Verifying and generating WP transformers for procedures on complex data
• Computing Preconditions and Postconditions of While Loops

Describes a project that uses

Uses Software

• ESC/Java
• SIMPLIFY

This page was built for publication: Efficient weakest preconditions

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