Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking

DOI10.1007/978-3-642-24372-1_24MaRDI QIDQ3172924zbMATH OpenOpenAlexFDO

Authors Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

Publication date 7 October 2011

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24372-1_24

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1696466
• Hybrid on-the-fly LTL model checking with the sweep-line method
• Tools and Algorithms for the Construction and Analysis of Systems
• LTL-model-checking via model composition
• LTL model checking of self modifying code
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• LTL Generalized Model Checking Revisited
• scientific article; zbMATH DE number 1670845
• scientific article; zbMATH DE number 1487868

Cited in

(1)

• Component-wise incremental LTL model checking

Describes a project that uses

Uses Software

• libDDD

This page was built for publication: Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking

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