Booster: An Acceleration-Based Verification Framework for Array Programs
From MaRDI portal
Publication:3457775
DOI10.1007/978-3-319-11936-6_2zbMath1448.68284OpenAlexW192687085MaRDI QIDQ3457775
Silvio Ghilardi, Francesco Alberti, 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
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (12)
Verifying Array Manipulating Programs with Full-Program Induction ⋮ Decision procedures for flat array properties ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Horn Clause Solvers for Program Verification ⋮ A New Acceleration-Based Combination Framework for Array Properties ⋮ On algebraic array theories ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Booster
Uses Software
This page was built for publication: Booster: An Acceleration-Based Verification Framework for Array Programs