Counterexample-guided focus

DOI10.1145/1706299.1706330MaRDI QIDQ5255078zbMATH OpenOpenAlexFDO

Authors Andreas Podelski, Thomas Wies

Publication date 11 June 2015

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

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

zbMATH Keywords

shape analysisdata structuresabstraction refinementpredicate abstractionquantified invariants

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Quantifiers on demand
• scientific article; zbMATH DE number 1953018
• Counterexample-guided precondition inference
• Predicate abstraction for software verification
• Quantified Heap Invariants for Object-Oriented Programs

Cited in

(10)

• An efficient decision procedure for imperative tree data structures
• How testing helps to diagnose proof failures
• Counterexample validation and interpolation-based refinement for forest automata
• Predicate abstraction for program verification
• Verification of heap manipulating programs with ordered data by extended forest automata
• Lazy slicing for state-space exploration
• Complete instantiation-based interpolation
• A shape graph logic and a shape system
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Towards Complete Reasoning about Axiomatic Specifications

This page was built for publication: Counterexample-guided focus

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