Functional specification of hardware via temporal logic

DOI10.1007/978-3-319-10575-8_24MaRDI QIDQ3176382zbMATH OpenOpenAlexFDO

Authors Cindy Eisner, Dana Fisman

Publication date 20 July 2018

Published in Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10575-8_24

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical problems of computer architecture (68M07) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 3982506
• scientific article; zbMATH DE number 2080056
• scientific article; zbMATH DE number 52331
• Using Temporal Logic to Analyse Temporal Logic: A Hierarchical Approach Based on Intervals
• On Regular Temporal Logics with Past,

Cites work

• A topological characterization of weakness
• Complete Proof System for QPTL
• Correct Hardware Design and Verification Methods
• Defining liveness
• Embedding finite automata within regular expressions
• From Church and Prior to PSL
• Hardware and Software, Verification and Testing
• scientific article; zbMATH DE number 1670800 (Why is no real title available?)
• scientific article; zbMATH DE number 1705164 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3848604 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3876574 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 4027441 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1956573 (Why is no real title available?)
• scientific article; zbMATH DE number 2038760 (Why is no real title available?)
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1796144 (Why is no real title available?)
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• scientific article; zbMATH DE number 2102708 (Why is no real title available?)
• scientific article; zbMATH DE number 2196589 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness
• Process logic with regular formulas
• Process logic: Expressiveness, decidability, completeness
• Propositional dynamic logic of regular programs
• Reasoning with temporal logic on truncated paths.
• Recognizing safety and liveness
• Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations
• Some Complexity Results for SystemVerilog Assertions
• Star-free regular sets of ω-sequences
• State complexity of chop operations on unary and finite languages
• Succinctness of Regular Expressions with Interleaving, Intersection and Counting
• Succinctness of the complement and intersection of regular expressions
• Temporal logic can be more expressive
• The complementation problem for Büchi automata with applications to temporal logic
• The complexity of propositional linear temporal logics
• Validating the PSL/Sugar semantics using automated reasoning

Cited in

(5)

• An application of temporal projection to interleaving concurrency
• Temporal logic and fair discrete systems
• SAT-Based Model Checking
• Automated Technology for Verification and Analysis
• Constraint LTL with remote access

Describes a project that uses

Uses Software

• FoCs

This page was built for publication: Functional specification of hardware via temporal logic

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