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

Formal languages and automata (68Q45) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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)

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

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)