swMATH ID: 33291
Software Authors: Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha
Description: Booster: an acceleration-based verification framework for array programs. We present Booster, a new framework developed for verifiying programs handling arrays. Booster integrates new acceleration features with standard verification techniques, like Lazy Abstraction with Interpolants (extended to arrays). The new acceleration features are the key for scaling-up in the verification of programs with arrays, allowing Booster to efficiently generate required quantified safe inductive invariants attesting the safety of the input code.
Homepage: https://link.springer.com/chapter/10.1007%2F978-3-319-11936-6_2
Related Software: Mcmt; SAFARI; z3; SMT-LIB; CVC4; FunArray; VERIFAS; Cubicle; ASASP; Yices; googletest; Yosys; Ivy; CoSA; Verilog2SMV; SPIN; PySMT; Sally; MathSAT5; NuSMV
Referenced in: 6 Publications

Referencing Publications by Year