Light-Weight SMT-based Model Checking

DOI10.1016/j.entcs.2009.08.019zbMath1335.68138OpenAlexW2034565311MaRDI QIDQ5178977

Thomas Valsecchi, Silvio Ranise, Silvio Ghilardi

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

safetysatisfiability modulo theoriesmodel checking of infinite-state systems

Mathematics Subject Classification ID

Related Items (2)

An extension of lazy abstraction with interpolation for programs with arrays ⋮ MCMT: A Model Checker Modulo Theories

Uses Software

• SMT-LIB
• z3

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• PFS Clustering Method
• Towards SMT Model Checking of Array-Based Systems
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• SHERLOCK HOLMES IN BABYLON
• On model checking data-independent systems with arrays without reset
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Rewriting Systems with Data
• Communicating Sequential Processes. The First 25 Years
• Computer Aided Verification
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Model Checking Software
• Perspectives of System Informatics

This page was built for publication: Light-Weight SMT-based Model Checking