On the Purpose of Event-B Proof Obligations

DOI10.1007/978-3-540-87603-8_11zbMath1156.68348OpenAlexW1883612199MaRDI QIDQ3535369

Stefan Hallerstede

Publication date: 11 November 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

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 (6)

Verifiable Code Generation from Scheduled Event-B Models ⋮ Building Specifications in the Event-B Institution ⋮ Experiments in program verification using Event-B ⋮ Proving Quicksort Correct in Event-B ⋮ Derivation of concurrent programs by stepwise scheduling of Event-B models ⋮ Incremental System Modelling in Event-B

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Refinement Calculus
• Data Refinement
• Unbounded nondeterminism in CSP

This page was built for publication: On the Purpose of Event-B Proof Obligations