Avoiding exponential explosion: generating compact verification conditions

DOI10.1145/360204.360220MaRDI QIDQ5178883zbMATH OpenOpenAlexFDO

Authors Cormac Flanagan, James B. Saxe

Publication date 17 March 2015

Published in Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/360204.360220

Mathematics Subject Classification ID

Theory of programming languages (68N15) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Effective generation of verification conditions for non-deterministic unstructured programs
• Verification Condition Generation Via Theorem Proving
• Verification conditions for source-level imperative programs
• Building verification condition generators by compositional extension
• Explaining Verification Conditions

Cited in

(23)

• Instrumenting a weakest precondition calculus for counterexample generation
• Automated verification of functional correctness of race-free GPU programs
• Assertion-based slicing and slice graphs
• Certified verification of relational properties
• Quantitative information flow as safety and liveness hyperproperties
• Faster and more complete extended static checking for the Java modeling language
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Effective generation of verification conditions for non-deterministic unstructured programs
• Computing Preconditions and Postconditions of While Loops
• Solving constrained Horn clauses using dependence-disjoint expansions
• Function extraction
• Verification conditions for source-level imperative programs
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Explaining Verification Conditions
• Modular verification of multithreaded programs
• Improving Generalization in Software IC3
• Symbolic encoding of LL(1) parsing and its applications
• Doomed program points
• Automatic program instrumentation for automatic verification
• Sound runtime assertion checking for memory properties via program transformation
• A program instrumentation framework for automatic verification
• Efficient weakest preconditions
• Generation of correctness conditions for imperative programs

This page was built for publication: Avoiding exponential explosion: generating compact verification conditions

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