Symbolic trajectory evaluation

DOI10.1007/978-3-319-10575-8_25MaRDI QIDQ3176383zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Formal Methods for Hardware Verification
• Symbolic trajectory evaluation for word-level verification: theory and implementation
• Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
• Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
• scientific article; zbMATH DE number 2102706

Cites work

• A Faithful Semantics for Generalised Symbolic Trajectory Evaluation
• A methodology for hardware verification based on logic simulation
• Abstraction and Refinement in Model Checking
• Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
• Computer Aided Verification
• Computer Aided Verification
• Efficient Automatic STE Refinement Using Responsibility
• Efficient detection of vacuity in temporal model checking
• Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
• Formal Methods for Hardware Verification
• GSTE is partitioned model checking
• Higher Order Logic and Hardware Verification
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 1979540 (Why is no real title available?)
• scientific article; zbMATH DE number 1979544 (Why is no real title available?)
• scientific article; zbMATH DE number 194916 (Why is no real title available?)
• scientific article; zbMATH DE number 1852159 (Why is no real title available?)
• scientific article; zbMATH DE number 1857502 (Why is no real title available?)
• scientific article; zbMATH DE number 2102706 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 6722179 (Why is no real title available?)
• Model checking
• Property-Driven Partitioning for Abstraction Refinement

Cited in

(13)

• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
• A Faithful Semantics for Generalised Symbolic Trajectory Evaluation
• scientific article; zbMATH DE number 1979544 (Why is no real title available?)
• scientific article; zbMATH DE number 1487865 (Why is no real title available?)
• scientific article; zbMATH DE number 2102706 (Why is no real title available?)
• Symbolic trajectory evaluation for word-level verification: theory and implementation
• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
• Efficient Automatic STE Refinement Using Responsibility
• Static Analysis
• Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
• Formal Methods for Hardware Verification
• Timed causal fanin analysis for symbolic simulation

Describes a project that uses

Uses Software

• ABC
• Haskell
• ML
• HOL

This page was built for publication: Symbolic trajectory evaluation

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