Model-checking systems with unbounded variables without abstraction

DOI10.1007/978-3-540-27815-3_11MaRDI QIDQ5312973zbMATH OpenOpenAlexFDO

Authors Magali Contensin, Laurence Pierre

Publication date 25 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98770

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2182497
• Bounded model checking of infinite state systems
• Verification of finite state systems by compositional model checking
• Model-Checking Large Finite-State Systems and Beyond
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)

Cited in

(3)

• Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables
• On model checking data-independent systems with arrays without reset
• An automata-theoretic approach for model-checking systems with unspecified components

Describes a project that uses

Uses Software

• PVS
• ACL2
• HOL
• InVeSt
• MOCHA

This page was built for publication: Model-checking systems with unbounded variables without abstraction

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