MLVR: Regular Expression-Based Specification for Verified Model Checking of Hardware
Model checking is an approach to verification of finite-state systems which relies on iterating through all possible states and checking whether some condition holds at each state. One challenge with this approach is that in the majority of real-world systems, the number of states to traverse is too...
Main Author: | Kammer, Gabriel A. |
---|---|
Other Authors: | Chlipala, Adam |
Format: | Thesis |
Published: |
Massachusetts Institute of Technology
2024
|
Online Access: | https://hdl.handle.net/1721.1/153899 |
Similar Items
-
Verifying Team Formation Protocols with Probabilistic Model Checking
by: Chen, T, et al.
Published: (2011) -
Verifying linearizability via optimized refinement checking
by: Dong, Jin Song, et al.
Published: (2013) -
The use of B to specify‚ design and verify hardware
by: Ifill, W, et al.
Published: (2001) -
JBMC: a bounded model checking tool for verifying Java bytecode
by: Cordeiro, L, et al.
Published: (2018) -
Verifying quantitative reliability for programs that execute on unreliable hardware
by: Misailovic, Sasa, et al.
Published: (2015)