Automatic symmetry detection for Promela

DOI10.1007/s10817-008-9107-4zbMath1191.68411OpenAlexW2144174074MaRDI QIDQ1040774

Alastair F. Donaldson, Alice Ann Miller

Publication date: 25 November 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-008-9107-4

zbMATH Keywords

model checkingsymmetry reductionautomatic verificationPromela

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Counterexample-guided abstraction refinement for symmetric concurrent programs

Uses Software

• GAP
• nauty
• TopSpin
• SPIN
• Uppaal
• SymmSpin
• PROMELA
• ETCH
• SymmExtractor
• Featherweight Java
• SableCC

Cites Work

• Uppaal in a nutshell
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Fundamental Approaches to Software Engineering
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item