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)

Full work available at URL https://doi.org/10.1007/978-3-031-22308-2_11

zbMATH Keywords

constrained Horn clausesmodular verificationpointer analysissoftware model checking

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

• Compositional shape analysis by means of bi-abduction
• Dafny: an automatic program verifier for functional correctness
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 3359806 (Why is no real title available?)
• 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)