Coverage metrics for temporal logic model checking

DOI10.1007/S10703-006-0001-6MaRDI QIDQ853721zbMATH OpenOpenAlexFDO

Authors Hana Chockler, Orna Kupferman, Moshe Y. Vardi

Publication date 17 November 2006

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

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.1552

zbMATH Keywords

AlgorithmsModel checkingFormal verificationCoverage metrics

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 1701778
• scientific article; zbMATH DE number 1796124
• scientific article; zbMATH DE number 2196601
• scientific article; zbMATH DE number 2080058
• Model-checking timed temporal logics
• scientific article; zbMATH DE number 1852156
• Model Checking Temporal Metric Specifications with Trio2Promela
• Correct Hardware Design and Verification Methods
• A model checker for linear time temporal logic

Cites work

• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 4012495 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1487861 (Why is no real title available?)
• scientific article; zbMATH DE number 1487867 (Why is no real title available?)
• scientific article; zbMATH DE number 1903373 (Why is no real title available?)
• scientific article; zbMATH DE number 918600 (Why is no real title available?)
• An automata-theoretic approach to branching-time model checking
• Correct Hardware Design and Verification Methods
• Correct Hardware Design and Verification Methods
• Efficient detection of vacuity in temporal model checking
• Enhanced vacuity detection in linear temporal logic.

Cited in

(11)

• Correct Hardware Design and Verification Methods
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• scientific article; zbMATH DE number 1852156 (Why is no real title available?)
• Sanity Checks in Formal Verification
• scientific article; zbMATH DE number 1701778 (Why is no real title available?)
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 1796124 (Why is no real title available?)
• Vacuity in practice: temporal antecedent failure
• Incremental design-space model checking via reusable reachable state approximations
• State coverage metrics for specification-based testing with Büchi automata
• Numerical coverage estimation for the symbolic simulation of real-time systems

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Coverage metrics for temporal logic model checking

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