Efficient modular SMT-based model checking of pointer programs

DOI10.1007/978-3-031-22308-2_11MaRDI QIDQ6164428zbMATH OpenFDO

Authors Isabel García-Contreras, Arie Gurfinkel, Jorge Navas

Publication date 28 July 2023

Published in Static Analysis (Search for Journal in Brave)

zbMATH Keywords

modular verificationsoftware model checkingpointer analysisconstrained Horn clauses

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

• SMT-based model checking for recursive programs
• Computer Science Logic
• Function summarization modulo theories
• RustHorn: CHC-based verification for Rust programs
• Unbounded procedure summaries from bounded environments

Cites work

• scientific article; zbMATH DE number 3359806 (Why is no real title available?)
• Compositional shape analysis by means of bi-abduction
• Dafny: an automatic program verifier for functional correctness
• Horn clause solvers for program verification
• ICE-based refinement type discovery for higher-order functional programs
• Nested interpolants
• Quantifiers on demand
• SMT-based model checking for recursive programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Viper: a verification infrastructure for permission-based reasoning
• Whale: an interpolation-based algorithm for inter-procedural verification

Cited in

(2)

• Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
• Computer Science Logic

This page was built for publication: Efficient modular SMT-based model checking of pointer programs

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