Syntax-directed model checking of sequential programs
From MaRDI portal
Publication:1858441
DOI10.1016/S1567-8326(02)00035-8zbMath1008.68075OpenAlexW2000953224MaRDI QIDQ1858441
Publication date: 13 February 2003
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s1567-8326(02)00035-8
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Uses Software
Cites Work
- Precise interprocedural dataflow analysis with applications to constant propagation
- The temporal semantics of concurrent programs
- Symbolic model checking: \(10^{20}\) states and beyond
- Model checking JAVA programs using JAVA PathFinder
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Graph-Based Algorithms for Boolean Function Manipulation
- “Sometimes” and “not never” revisited
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Syntax-directed model checking of sequential programs