Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems

DOI10.1007/978-3-540-73595-3_25MaRDI QIDQ3608784zbMATH OpenOpenAlexFDO

Authors Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73595-3_25

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1499079
• scientific article; zbMATH DE number 1263840
• A decidability result for the model checking of infinite-state systems
• scientific article; zbMATH DE number 2102702
• Decidability of model checking for infinite-state concurrent systems
• Bounded model checking of infinite state systems
• Computer Aided Verification
• Equivalence-checking with infinite-state systems: techniques and results
• Equivalence-checking on infinite-state systems: Techniques and results

Cited in

(14)

• CTL* model checking for data-aware dynamic systems with arithmetic
• SMT-based scenario verification for hybrid systems
• SMT-based verification of data-aware processes: a model-theoretic approach
• A decidable and expressive fragment of many-sorted first-order linear temporal logic
• A decidability result for the model checking of infinite-state systems
• IPL: an integration property language for multi-model cyber-physical systems
• Model checking parameterised multi-token systems via the composition method
• Satisfiability modulo theories
• Hierarchical reasoning for the verification of parametric systems
• scientific article; zbMATH DE number 1617315 (Why is no real title available?)
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Rewriting modulo SMT and open system analysis
• Linear-time temporal logic with event freezing functions
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

This page was built for publication: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems

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