An automatic abstraction technique for verifying featured, parameterised systems
From MaRDI portal
Publication:947791
DOI10.1016/j.tcs.2008.03.034zbMath1293.68191WikidataQ59675362 ScholiaQ59675362MaRDI QIDQ947791
Muffy Calder, Alice Ann Miller
Publication date: 7 October 2008
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: http://eprints.gla.ac.uk/40516/1/40516.pdf
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Model checking learning agent systems using Promela with embedded C code and abstraction, Temporal Verification of Fault-Tolerant Protocols
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Reasoning about networks with many identical finite state processes
- Characterizing finite Kripke structures in propositional temporal logic
- Computer aided verification. 5th international conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993. Proceedings
- A structural induction theorem for processes
- Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
- Verifying programs with unreliable channels
- Counterexample-guided abstraction refinement for symbolic model checking
- Reasoning about systems with many processes
- Interpolants and Symbolic Model Checking
- Objects, Agents, and Features
- FM 2005: Formal Methods
- Automatic verification of parameterized networks of processes