Symbolic Trajectory Evaluation

DOI10.1007/978-3-319-10575-8_25zbMath1392.68261OpenAlexW2803544309MaRDI QIDQ3176383

Tom Melham

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_25

Mathematics Subject Classification ID

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

Uses Software

• ML
• Haskell
• HOL
• ABC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• GSTE is partitioned model checking
• Higher Order Logic and Hardware Verification
• Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
• Abstraction and Refinement in Model Checking
• A Faithful Semantics for Generalised Symbolic Trajectory Evaluation
• A methodology for hardware verification based on logic simulation
• Computer Aided Verification
• Efficient Automatic STE Refinement Using Responsibility
• Computer Aided Verification
• Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
• Property-Driven Partitioning for Abstraction Refinement
• Formal Methods for Hardware Verification
• Efficient detection of vacuity in temporal model checking

This page was built for publication: Symbolic Trajectory Evaluation