Vacuity in practice: temporal antecedent failure

DOI10.1007/s10703-014-0221-0zbMath1322.68132OpenAlexW2019065032MaRDI QIDQ2018060

Dana Fisman, Shoham Ben-David, Sitvanit Ruah, Fady Copty

Publication date: 24 March 2015

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-014-0221-0

zbMATH Keywords

regular expressionsmodel checkingtemporal logicvacuityforward NFAPSL/SVA

Mathematics Subject Classification ID

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

Related Items

Foundations of fine-grained explainability

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• From regular expressions to deterministic automata
• Coverage metrics for temporal logic model checking
• Embedding finite automata within regular expressions
• Before and after vacuity
• Beyond vacuity: towards the strongest passing formula
• Vacuity Checking in the Modal Mu-Calculus*
• SAT-Based Model Checking without Unrolling
• THE ABSTRACT THEORY OF AUTOMATA
• On the Notion of Vacuous Truth
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Lattice Automata
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• Sanity Checks in Formal Verification
• Hardware and Software, Verification and Testing
• Computer Aided Verification
• Efficient detection of vacuity in temporal model checking