Efficient modular SMT-based model checking of pointer programs

DOI10.1007/978-3-031-22308-2_11zbMATH Open1524.68190MaRDI QIDQ6164428FDOQ6164428

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

Publication date: 28 July 2023

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

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

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)

Cites Work

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

Cited In (2)

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

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)