Functional Specification of Hardware via Temporal Logic

DOI10.1007/978-3-319-10575-8_24zbMath1392.68247OpenAlexW2804949216MaRDI QIDQ3176382

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

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

Related Items (3)

Temporal Logic and Fair Discrete Systems ⋮ SAT-Based Model Checking ⋮ An application of temporal projection to interleaving concurrency

Uses Software

• FoCs

Cites Work

• Validating the PSL/Sugar semantics using automated reasoning
• Embedding finite automata within regular expressions
• Process logic with regular formulas
• Defining liveness
• The complementation problem for Büchi automata with applications to temporal logic
• Recognizing safety and liveness
• Process logic: Expressiveness, decidability, completeness
• Propositional dynamic logic of regular programs
• State Complexity of Chop Operations on Unary and Finite Languages
• Temporal logic can be more expressive
• From Church and Prior to PSL
• Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness
• Succinctness of Regular Expressions with Interleaving, Intersection and Counting
• The complexity of propositional linear temporal logics
• Star-free regular sets of ω-sequences
• Complete Proof System for QPTL
• Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations
• A topological characterization of weakness
• Correct Hardware Design and Verification Methods
• Some Complexity Results for SystemVerilog Assertions
• Hardware and Software, Verification and Testing
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Functional Specification of Hardware via Temporal Logic