Booster: an acceleration-based verification framework for array programs

DOI10.1007/978-3-319-11936-6_2MaRDI QIDQ3457775zbMATH OpenOpenAlexFDO

Authors Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Publication date 17 December 2015

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-11936-6_2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A new acceleration-based combination framework for array properties
• Automatic Verification of Integer Array Programs
• An extension of lazy abstraction with interpolation for programs with arrays
• Lazy abstraction with interpolants for arrays
• Verifying array manipulating programs by tiling

Cited in

(13)

• Verifying array manipulating programs with full-program induction
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Interpolation and amalgamation for arrays with MaxDiff
• SMT-based verification of data-aware processes: a model-theoretic approach
• Decision procedures for flat array properties
• Adding decision procedures to SMT solvers using axioms with triggers
• Horn clause solvers for program verification
• A new acceleration-based combination framework for array properties
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Booster
• On algebraic array theories
• \(Booster\): A high-level language for portable parallel algorithms
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

Describes a project that uses

Uses Software

• FunArray

This page was built for publication: Booster: an acceleration-based verification framework for array programs

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