Towards SMT Model Checking of Array-Based Systems

DOI10.1007/978-3-540-71070-7_6zbMath1165.68406OpenAlexW1511903507MaRDI QIDQ3541687

Daniele Zucchelli, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Satisfiability Modulo Theories, Rewriting modulo SMT and open system analysis, SMT-based generation of symbolic automata, Exploiting step semantics for efficient bounded model checking of asynchronous systems, Towards SMT Model Checking of Array-Based Systems, SMT-based verification of data-aware processes: a model-theoretic approach, Light-Weight SMT-based Model Checking, MCMT: A Model Checker Modulo Theories, Generalized rewrite theories, coherence completion, and symbolic methods, Universal invariant checking of parametric systems with quantifier-free SMT reasoning, Taming past LTL and flat counter systems, Finite reasons for safety

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient theory combination via Boolean search
• Solving SAT and SAT Modulo Theories
• Towards SMT Model Checking of Array-Based Systems
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Rewriting Systems with Data
• On Local Reasoning in Verification
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Verification, Model Checking, and Abstract Interpretation
• Perspectives of System Informatics
• Symbolic model checking with rich assertional languages