Empowering the Event-B method using external theories

DOI10.1007/978-3-031-07727-2_2zbMath1502.68176OpenAlexW4285159108MaRDI QIDQ2165497

Marc Pantel, Neeraj Kumar Singh, Yamine Ait-Ameur, Ismail Mendil, Peter Rivière, Dominique Méry, Guillaume Dupont

Publication date: 19 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-07727-2_2

zbMATH Keywords

safetyEvent-Bwell-definednessinvariants preservationpartial definitionsstate-based methods

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial functions and logics: A warning
• A logic covering undefinedness in program proofs
• Comments on ``On the proof of a distributed algorithm: Always-true is not invariant
• A typed logic of partial functions reconstructed classically
• Isabelle/HOL. A proof assistant for higher-order logic
• Practical Theory Extension in Event-B
• Guarded commands, nondeterminacy and formal derivation of programs
• The B-Book
• Abstract State Machines
• An axiomatic basis for computer programming

This page was built for publication: Empowering the Event-B method using external theories