Regression verification for unbalanced recursive functions

DOI10.1007/978-3-319-48989-6_39zbMath1427.68055OpenAlexW2554831868MaRDI QIDQ2281656

Maor Veitsman, Ofer Strichman

Publication date: 3 January 2020

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

Mathematics Subject Classification ID

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

Related Items (7)

Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Unnamed Item ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Bridging arrays and ADTs in recursive proofs ⋮ A self-certifying compilation framework for WebAssembly ⋮ Predicate Pairing for program verification ⋮ RVT

Uses Software

• z3
• Boogie
• SymDiff
• SeaHorn

This page was built for publication: Regression verification for unbalanced recursive functions