On the purpose of Event-B proof obligations

DOI10.1007/S00165-009-0138-3zbMath1214.68135OpenAlexW2070694647MaRDI QIDQ539230

Stefan Hallerstede

Publication date: 27 May 2011

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://eprints.soton.ac.uk/266052/1/evtbena.pdf

zbMATH Keywords

semanticsproofEvent-Bproof obligation

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

External and internal choice with event groups in Event-B ⋮ The behavioural semantics of Event-B refinement

Uses Software

• Rodin
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the shape of mathematical arguments
• A mechanically proved and incremental development of IEEE 1394 tree identify protocol
• Stepwise refinement of communicating systems
• Qualitative Probabilistic Modelling in Event-B
• The B-Book

This page was built for publication: On the purpose of Event-B proof obligations