An automatic abstraction technique for verifying featured, parameterised systems

DOI10.1016/j.tcs.2008.03.034zbMath1293.68191OpenAlexW2003699411WikidataQ59675362 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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Model checking learning agent systems using Promela with embedded C code and abstraction ⋮ Temporal Verification of Fault-Tolerant Protocols

Uses Software

• SPIN
• Cadence SMV

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An automatic abstraction technique for verifying featured, parameterised systems