Light-weight SMT-based model checking

DOI10.1016/J.ENTCS.2009.08.019MaRDI QIDQ5178977zbMATH OpenOpenAlexFDO

Authors Silvio Ghilardi, Silvio Ranise, Thomas Valsecchi

Publication date 18 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.08.019

zbMATH Keywords

model checking of infinite-state systemssafetysatisfiability modulo theories

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed algorithms (68W15)

Recommendations

• Towards SMT Model Checking of Array-Based Systems
• MCMT: a model checker modulo theories
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Verification of SMT systems with quantifiers
• SMT-based model checking for recursive programs

Cites work

• A logical reconstruction of reachability
• Communicating Sequential Processes. The First 25 Years
• Computer Aided Verification
• Efficient E-Matching for SMT Solvers
• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 3550519 (Why is no real title available?)
• scientific article; zbMATH DE number 2080048 (Why is no real title available?)
• scientific article; zbMATH DE number 1905119 (Why is no real title available?)
• scientific article; zbMATH DE number 2090318 (Why is no real title available?)
• Lazy satisfiability modulo theories
• Model Checking Software
• On model checking data-independent systems with arrays without reset
• Parameterized Verification of Infinite-State Processes with Global Conditions
• PFS Clustering Method
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Rewriting Systems with Data
• SHERLOCK HOLMES IN BABYLON
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Towards SMT Model Checking of Array-Based Systems

Cited in

(9)

• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Advanced SMT techniques for weighted model integration
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Towards SMT Model Checking of Array-Based Systems
• An extension of lazy abstraction with interpolation for programs with arrays
• SMT-based verification of data-aware processes: a model-theoretic approach
• SMT-based model checking for recursive programs
• MCMT: a model checker modulo theories
• Verification of SMT systems with quantifiers

Describes a project that uses

Uses Software

• z3
• SMT-LIB

This page was built for publication: Light-weight SMT-based model checking

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