Vacuity in practice: temporal antecedent failure

DOI10.1007/S10703-014-0221-0MaRDI QIDQ2018060zbMATH OpenOpenAlexFDO

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

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

model checkingtemporal logicregular expressionsvacuityforward NFAPSL/SVA

Mathematics Subject Classification ID

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

Recommendations

• Temporal Antecedent Failure: Refining Vacuity
• Before and after vacuity
• Enhanced vacuity detection in linear temporal logic.
• Efficient detection of vacuity in temporal model checking
• scientific article; zbMATH DE number 1487861

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 5353387 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 2081113 (Why is no real title available?)
• scientific article; zbMATH DE number 1487861 (Why is no real title available?)
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• scientific article; zbMATH DE number 1903373 (Why is no real title available?)
• scientific article; zbMATH DE number 3251424 (Why is no real title available?)
• Before and after vacuity
• Beyond vacuity: towards the strongest passing formula
• Computer Aided Verification
• Correct Hardware Design and Verification Methods
• Coverage metrics for temporal logic model checking
• Efficient detection of vacuity in temporal model checking
• Embedding finite automata within regular expressions
• Enhanced vacuity detection in linear temporal logic.
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• From regular expressions to deterministic automata
• Hardware and Software, Verification and Testing
• Lattice Automata
• On the Notion of Vacuous Truth
• SAT-Based Model Checking without Unrolling
• Sanity Checks in Formal Verification
• THE ABSTRACT THEORY OF AUTOMATA
• Tools and Algorithms for the Construction and Analysis of Systems
• Vacuity checking in the modal mu-calculus

Cited in

(5)

• Foundations of fine-grained explainability
• Temporal Antecedent Failure: Refining Vacuity
• Vacuity checking in the modal mu-calculus
• Before and after vacuity
• On the Notion of Vacuous Truth

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Vacuity in practice: temporal antecedent failure

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