Automatic Verification of Integer Array Programs

DOI10.1007/978-3-642-02658-4_15MaRDI QIDQ3636859zbMATH OpenOpenAlexFDO

Authors Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konečný, Tomáš Vojnar

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying Array Programs by Transforming Verification Conditions
• Verification problem for linear programs with Boolean arrays
• A rule-based verification strategy for array manipulating programs
• Verifying array manipulating programs by tiling
• Algorithmic analysis of array-accessing programs

Cited in

(18)

• Cell morphing: from array programs to array-free Horn clauses
• Verification problem for linear programs with Boolean arrays
• Property checking array programs using loop shrinking
• Array theory of bounded elements and its applications
• Automaton-based array initialization analysis
• Verifying Array Programs by Transforming Verification Conditions
• Algorithmic analysis of array-accessing programs
• Guiding Craig interpolation with domain-specific abstractions
• A rule-based verification strategy for array manipulating programs
• Booster: an acceleration-based verification framework for array programs
• Inferring Loop Invariants Using Postconditions
• Algorithmic Analysis of Array-Accessing Programs
• Verifying array manipulating programs with full-program induction
• Computing exact loop bounds for bounded program verification
• Verifying array manipulating programs by tiling
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• Automatic program instrumentation for automatic verification
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants

This page was built for publication: Automatic Verification of Integer Array Programs

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