An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking

DOI10.1007/978-3-540-93900-9_23zbMATH Open1206.68190OpenAlexW1896342373MaRDI QIDQ3600481FDOQ3600481

Authors: Rotem Oshman 

Publication date: 10 February 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-540-93900-9_23

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• On the magnitude of completeness thresholds in bounded model checking
• Bounded model checking for timed automata
• Linear completeness thresholds for bounded model checking
• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
• Bounded Model Checking for Parametric Timed Automata
• Automata-Theoretic Model Checking Revisited
• Bounded Model Checking for Weak Alternating Büchi Automata

Mathematics Subject Classification ID

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

Cited In (8)

• Dynamic input/output automata: a formal and compositional model for dynamic systems
• On the magnitude of completeness thresholds in bounded model checking
• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
• Bounded model checking with SNF, alternating automata, and Büchi automata
• Linear completeness thresholds for bounded model checking
• Formal Approaches to Software Testing
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• The firing squad problem revisited

This page was built for publication: An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking

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