A local approach for temporal model checking of Java bytecode
From MaRDI portal
Publication:1776379
DOI10.1016/j.jcss.2004.11.001zbMath1068.68082MaRDI QIDQ1776379
Antonella Santone, Gigliola Vaglini
Publication date: 12 May 2005
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2004.11.001
Model checking; Temporal logic; Software systems; Formula-based abstractions; Symbolic computations; Tableau systems
68N15: Theory of programming languages
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Abstract reduction in directed model checking CCS processes
- Tableau-based model checking in the propositional mu-calculus
- Local model checking in the modal mu-calculus
- Local model checking for infinite state spaces
- Slicing software for model construction
- A local approach for temporal model checking of Java bytecode
- Model checking JAVA programs using JAVA PathFinder
- Selective mu-calculus and formula-based equivalence of transition systems
- Lazy abstraction
- Model Checking Software
- Interpolants and Symbolic Model Checking
