The B-Book
From MaRDI portal
Publication:4208552
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; zbMATH DE number 49477
- 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
Cited in
(only showing first 100 items - show all)- Incremental System Modelling in Event-B
- Finding Counter Examples in Induction Proofs
- Unifying Sets and Programs via Dependent Types
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Specification and refinement of mobile systems in MTLA and mobile UML
- An Event-B based approach for cloud composite services verification
- iRho: an imperative rewriting calculus
- Integrating simplex with tableaux
- Knowledge representation analysis of graph mining
- scientific article; zbMATH DE number 2172802 (Why is no real title available?)
- Schematic program proofs with abstract execution. Theory and applications
- Modelling of Complex Software Systems: A Reasoned Overview
- Test generation from event system abstractions to cover their states and transitions
- Action systems in incremental and aspect-oriented modeling
- From Sets to Bits in Coq
- Bunch theory: axioms, logic, applications and model
- Splitting atoms safely
- Unifying sets and programs via dependent types
- Responsiveness and stable revivals
- 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
- Formalization of an architectural model for exception handling coordination based on CA action concepts
- Extending rely-guarantee thinking to handle real-time scheduling
- An extendible language for database schema refinement transformations
- Verifying a signature architecture: a comparative case study
- ASM refinement and generalizations of forward simulation in data refinement: a comparison
- A behavioural theory of recursive algorithms
- rCOS: defining meanings of component-based software architectures
- Verified Compilation and the B Method: A Proposal and a First Appraisal
- Spot the difference: a detailed comparison between B and Event-B
- The seven virtues of simple type theory
- Composing model programs for analysis
- Incremental parametric development of greedy algorithms
- Trace preservation in B and Event-B refinements
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B
- B: Towards zero defect software
- Operational semantics of the Java Card Virtual Machine
- A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case
- Balancing expressiveness in formal approaches to concurrency
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types
- A functional framework for agent-based models of exchange
- Tank monitoring: A pAMN case study
- Encapsulating deontic and branching time specifications
- scientific article; zbMATH DE number 2013599 (Why is no real title available?)
- Manipulating algebraic specifications with term-based and graph-based representations
- Elucidating concurrent algorithms via layers of abstraction and reification
- Combining Decision Procedures by (Model-)Equality Propagation
- A new roadmap for linking theories of programming
- 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
- Query-driven verification of data integration in the RDF data model
- Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm
- Modeling and visualizing object-oriented programs with Codecharts
- Modular verification of programs with effects and effect handlers in Coq
- Why Would You Trust B?
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Concurrent abstract state machines
- Theorem proving graph grammars with attributes and negative application conditions
- 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
- Predicate diagrams for the verification of real-time systems
- Mutation testing in UTP
- 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
- scientific article; zbMATH DE number 1615249 (Why is no real title available?)
- ASM-based formal design of an adaptivity component for a cloud system
- Modelling timed reactive systems from natural-language requirements
- Combining refinement and signal-temporal logic for biological systems
- Transposing partial components--an exercise on coalgebraic refinement
- Domain-specific semantics and data refinement of object models
- Discussion on: ``Formal specification method for systems automation
- Invariant-driven specifications in Maude
- A formal framework for specifying and analyzing logs as electronic evidence
- Specification of a localization component driven by a goal-based approach: some lessons we learned
- Integrating formal specifications into applications: the ProB Java API
- A refinement-based formal development of cyber-physical railway signalling systems
- Abstract state machines: a unifying view of models of computation and of system design frameworks
- Linking event-B and concurrent object-oriented programs
- Security invariants in discrete transition systems
- General refinement. I: Interfaces, determinism and special refinement
- Computation, hypercomputation, and physical science
- Pliant modalities in hybrid Event-B
- Possible values: exploring a concept for concurrency
- Model checking action system refinements
- scientific article; zbMATH DE number 2013582 (Why is no real title available?)
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)
