The B-Book

DOI10.1017/CBO9780511624162zbMATH Open0915.68015OpenAlexW4254354208MaRDI QIDQ4208552FDOQ4208552

Jean-Raymond Abrial

Publication date: 6 September 1998

Full work available at URL: https://doi.org/10.1017/cbo9780511624162

Recommendations

• Theories of programming. The life and works of Tony Hoare
• scientific article; zbMATH DE number 3909708
• scientific article; zbMATH DE number 439891
• A view of programming languages as symbiosis of meaning and computations
• Publication:3026308
• scientific article
• Theory of program structures: schemes, semantics, verification. 2nd printing
• Programming logics. Essays in memory of Harald Ganzinger
• Computational Semantics with Functional Programming, by Jan van Eijck and Christina Unger .
• The axiomatic semantics of programs based on Hoare's logic

zbMATH Keywords

B method

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01)

Cited In (only showing first 100 items - show all)

• Modelling of Complex Software Systems: A Reasoned Overview
• Responsiveness and stable revivals
• Splitting atoms safely
• Unifying sets and programs via dependent types
• Generating tests from B specifications and dynamic selection criteria
• On the purpose of Event-B proof obligations
• Retrenchment for Event-B: UseCase-wise development and Rodin integration
• Z2SAL: a translation-based model checker for Z
• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• The seven virtues of simple type theory
• Composing model programs for analysis
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B
• A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
• Balancing expressiveness in formal approaches to concurrency
• Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types
• A functional framework for agent-based models of exchange
• Encapsulating deontic and branching time specifications
• Combining Decision Procedures by (Model-)Equality Propagation
• Specification and Runtime Verification of Java Card Programs
• Elucidating concurrent algorithms via layers of abstraction and reification
• Fixpoints and Search in PVS
• Compositional noninterference from first principles
• Experiments in program verification using Event-B
• Mechanised support for sound refinement tactics
• Verification of distributed systems with local-global predicates
• Connectors as designs: modeling, refinement and test case generation
• Using formal methods with SysML in aerospace design and engineering
• Combining decision procedures by (model-)equality propagation
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Concurrent abstract state machines
• Mutation testing in UTP
• Compositionality: Ontology and Mereology of Domains
• ASM-based formal design of an adaptivity component for a cloud system
• Modelling timed reactive systems from natural-language requirements
• Transposing partial components--an exercise on coalgebraic refinement
• Abstract state machines: a unifying view of models of computation and of system design frameworks
• Relational concurrent refinement. II: Internal operations and outputs
• Model checking RAISE applicative specifications
• JCML: A specification language for the runtime verification of Java card programs
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• ELAN from a rewriting logic point of view
• Generic tools via general refinement
• The behavioural semantics of Event-B refinement
• Operating system verification---an overview
• A system for compositional verification of asynchronous objects
• A compositional automata-based semantics and preserving transformation rules for testing property patterns
• Generating Tests from B Specifications and Test Purposes
• Moded and continuous abstract state machines
• On Automating the Calculus of Relations
• The Composition of Event-B Models
• Specification and verification challenges for sequential object-oriented programs
• Generating counterexamples for quantitative safety specifications in probabilistic B
• The connection between two ways of reasoning about partial functions
• Preservation of probabilistic information flow under refinement
• Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B
• How to Brew-up a Refinement Ordering
• Patterns for Refinement Automation
• Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
• Temporal-logic property preservation under Z refinement
• Automating Event-B invariant proofs by rippling and proof patching
• Components as coalgebras: the refinement dimension
• Manifest domains: analysis and description
• On the Purpose of Event-B Proof Obligations
• Efficient Well-Definedness Checking
• Incremental System Modelling in Event-B
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Translating controlled graph grammars to ordinary graph grammars
• Specification and refinement of mobile systems in MTLA and mobile UML
• An Event-B based approach for cloud composite services verification
• Title not available (Why is that?)
• From Sets to Bits in Coq
• Set-Theoretic Models of Computations
• Formalization of an architectural model for exception handling coordination based on CA action concepts
• Verifying a signature architecture: a comparative case study
• Spot the difference: a detailed comparison between B and Event-B
• Operational semantics of the Java Card Virtual Machine
• Tank monitoring: A pAMN case study
• Manipulating algebraic specifications with term-based and graph-based representations
• Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving
• Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm
• Modular verification of programs with effects and effect handlers in Coq
• Integrating Simplex with Tableaux
• Experimenting Formal Proofs of Petri Nets Refinements
• Fully abstract models and refinements as tools to compare agents in timed coordination languages
• Automated proof of Bell-LaPadula security properties
• Optimising the ProB model checker for B using partial order reduction
• Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
• On integrating confidentiality and functionality in a formal method
• Kaisa Sere: in memoriam
• Refinement patterns for ASTDs
• Test-data generation for control coverage by proof
• Domain-specific semantics and data refinement of object models
• Integrating formal specifications into applications: the ProB Java API
• Invariant-driven specifications in Maude
• Security invariants in discrete transition systems
• Computation, hypercomputation, and physical science
• Title not available (Why is that?)

This page was built for publication: The B-Book

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