A local approach for temporal model checking of Java bytecode
From MaRDI portal
Publication:1776379
DOI10.1016/j.jcss.2004.11.001zbMath1068.68082OpenAlexW1979458401MaRDI 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 checkingTemporal logicSoftware systemsFormula-based abstractionsSymbolic computationsTableau systems
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)
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