An automatic abstraction technique for verifying featured, parameterised systems

DOI10.1016/J.TCS.2008.03.034MaRDI QIDQ947791zbMATH OpenOpenAlexWikidataFDO

Authors M. Calder, Alice 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

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

Recommendations

• Model checking and abstraction to the aid of parameterized systems (a survey)
• scientific article; zbMATH DE number 1953016
• View abstraction for systems with component identities
• Computer Aided Verification
• Compositional analysis for verification of parameterized systems

Cites work

• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1670785 (Why is no real title available?)
• scientific article; zbMATH DE number 522852 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1927557 (Why is no real title available?)
• scientific article; zbMATH DE number 1744963 (Why is no real title available?)
• scientific article; zbMATH DE number 1418468 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• A structural induction theorem for processes
• Automatic verification of parameterized networks of 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
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• Counterexample-guided abstraction refinement for symbolic model checking
• FM 2005: Formal Methods
• Interpolants and Symbolic Model Checking
• Objects, Agents, and Features
• Reasoning about networks with many identical finite state processes
• Reasoning about systems with many processes
• Verifying programs with unreliable channels

Cited in

(3)

• Temporal Verification of Fault-Tolerant Protocols
• Assertion-based analysis via slicing withABETS(system description)
• Model checking learning agent systems using Promela with embedded C code and abstraction

Describes a project that uses

Uses Software

• Cadence SMV
• SPIN

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q947791)