Efficient modular SMT-based model checking of pointer programs

DOI10.1007/978-3-031-22308-2_11zbMath1524.68190MaRDI QIDQ6164428

Arie Gurfinkel, Jorge A. Navas, Isabel García-Contreras

Publication date: 28 July 2023

Published in: Static Analysis (Search for Journal in Brave)

zbMATH Keywords

pointer analysismodular verificationsoftware model checkingconstrained Horn clauses

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• SMT-based model checking for recursive programs
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
• Horn Clause Solvers for Program Verification
• Dafny: An Automatic Program Verifier for Functional Correctness
• Nested interpolants
• Compositional shape analysis by means of bi-abduction
• Tools and Algorithms for the Construction and Analysis of Systems
• ICE-based refinement type discovery for higher-order functional programs
• Quantifiers on demand

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