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
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
