Efficient weakest preconditions

DOI10.1016/j.ipl.2004.10.015zbMath1173.68563OpenAlexW2164419371MaRDI QIDQ835051

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

formal semanticsautomatic theorem provingprogram correctness

Mathematics Subject Classification ID

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

Related Items (14)

Improving Generalization in Software IC3 ⋮ Backward symbolic execution with loop folding ⋮ Instrumenting a weakest precondition calculus for counterexample generation ⋮ Horn Clause Solvers for Program Verification ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Knowledge forgetting in propositional \(\mu\)-calculus ⋮ Doomed program points ⋮ Function extraction ⋮ Verification conditions for source-level imperative programs ⋮ Quantitative information flow as safety and liveness hyperproperties ⋮ Weakest Invariant Generation for Automated Addition of Fault-Tolerance ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ Computing Preconditions and Postconditions of While Loops ⋮ Verifying Whiley programs with Boogie

Uses Software

• SIMPLIFY
• ESC/Java

Cites Work

• Unnamed Item
• Combining angels, demons and miracles in program specifications
• Correct and Robust Programs
• Simplify: a theorem prover for program checking
• Programming as a Discipline of Mathematical Nature
• Avoiding exponential explosion

This page was built for publication: Efficient weakest preconditions