Temporal property verification as a program analysis task
From MaRDI portal
Publication:2441713
DOI10.1007/s10703-012-0153-5zbMath1284.68171OpenAlexW1518606372MaRDI QIDQ2441713
Byron Cook, Moshe Y. Vardi, Eric Koskinen
Publication date: 28 March 2014
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.357.2668
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (5)
Automatic discovery of fair paths in infinite-state transition systems ⋮ Unnamed Item ⋮ Temporal property verification as a program analysis task ⋮ The virtues of idleness: a decidable fragment of resource agent logic ⋮ \textsc{LTL} falsification in infinite-state systems
Uses Software
Cites Work
- Protocol conformance through refinement mappings in cadence SMV
- Symbolic model checking: \(10^{20}\) states and beyond
- Temporal property verification as a program analysis task
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation
- Variance analyses from invariance analyses
- Proving that programs eventually do something good
- Arithmetic Strengthening for Shape Analysis
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Compositional shape analysis by means of bi-abduction
- An automata-theoretic approach to branching-time model checking
- Making prophecies with decision predicates
- State/Event Software Verification for Branching-Time Specifications
- Automata, Languages and Programming
- Verification, Model Checking, and Abstract Interpretation
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Temporal property verification as a program analysis task
