A note on on-the-fly verification algorithms

DOI10.1007/B107194MaRDI QIDQ5703757zbMATH OpenOpenAlexFDO

Authors Stefan Schwoon, Javier Esparza

Publication date 10 November 2005

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

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• More efficient on-the-fly LTL verification with Tarjan's algorithm
• Tools and Algorithms for the Construction and Analysis of Systems
• Comparison of algorithms for checking emptiness on Büchi automata
• Truly on-the-fly LTL model checking
• On-the-fly verification of linear temporal logic

Cited in

(26)

• Refinement to imperative HOL
• On-the-fly diagnosability analysis of bounded and unbounded labeled Petri nets using verifier nets
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• Matching in security-by-contract for mobile code
• Model checking with fairness assumptions using PAT
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• Efficient verification algorithms for one-counter processes
• Comparison of algorithms for checking emptiness on Büchi automata
• Refinement to Imperative/HOL
• scientific article; zbMATH DE number 5540316 (Why is no real title available?)
• Edmonds-Karp
• Flow Networks
• CAVA LTL Modelchecker
• Gabow SCC
• On-the-fly verification of linear temporal logic
• Efficient emptiness check for timed Büchi automata
• scientific article; zbMATH DE number 2147038 (Why is no real title available?)
• Automated verification of parallel nested DFS
• Tools and Algorithms for the Construction and Analysis of Systems
• Prpu_Maxflow
• From LTL to rLTL monitoring: improved monitorability through robust semantics
• Flash memory efficient LTL model checking
• How hard is finding shortest counter-example lassos in model checking?
• A truly symbolic linear-time algorithm for SCC decomposition
• Model checking \(\omega \)-regular properties with decoupled search

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: A note on on-the-fly verification algorithms

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