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)

• 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?)
• Model checking action system refinements
• Semantics, calculi, and analysis for object-oriented specifications
• A New Roadmap for Linking Theories of Programming
• Toward a theory of program repair
• Refinement-Based Verification of Interactive Real-Time Systems
• Empowering the Event-B method using external theories
• Operation caching and state compression for model checking of high-level models. How to have your cake and eat it
• Interactive tool support for CSP \(\parallel\) B consistency checking
• Integrating stochastic reasoning into Event-B development
• Satisfiability in composition-nominative logics
• Stepwise refinement of heap-manipulating code in Chalice
• Abstractions of non-interference security: probabilistic versus possibilistic
• A Behavioural Theory of Recursive Algorithms
• Developing topology discovery in Event-B
• An Automation-Friendly Set Theory for the B Method
• A calculus for schemas in Z
• Model-Based Testing for Functional and Security Test Generation
• Automated reasoning with restricted intensional sets
• Unifying Theories of Programming in Isabelle
• Directed Model Checking for B: An Evaluation and New Techniques
• Finding Counter Examples in Induction Proofs
• BGSL: an imperative language for specification and refinement of backtracking programs
• iRho: an imperative rewriting calculus
• 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

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)