The B-Book
From MaRDI portal
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
- scientific article; zbMATH DE number 4013993
- 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)- Fully abstract models and refinements as tools to compare agents in timed coordination languages
- Model checking action system refinements
- Relational concurrent refinement. II: Internal operations and outputs
- Mutation testing in UTP
- Operating system verification---an overview
- Developing topology discovery in Event-B
- A calculus for schemas in Z
- ELAN from a rewriting logic point of view
- Abstract state machines: a unifying view of models of computation and of system design frameworks
- Operational semantics of the Java Card Virtual Machine
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Manipulating algebraic specifications with term-based and graph-based representations
- Temporal-logic property preservation under Z refinement
- Stepwise refinement of heap-manipulating code in Chalice
- Security invariants in discrete transition systems
- A system for compositional verification of asynchronous objects
- Abstractions of non-interference security: probabilistic versus possibilistic
- Modular verification of programs with effects and effect handlers in Coq
- Automated proof of Bell-LaPadula security properties
- BGSL: an imperative language for specification and refinement of backtracking programs
- Moded and continuous abstract state machines
- Spot the difference: a detailed comparison between B and Event-B
- Integrating formal specifications into applications: the ProB Java API
- 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
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Test generation from event system abstractions to cover their states and transitions
- Modeling and visualizing object-oriented programs with Codecharts
- Knowledge representation analysis of graph mining
- Theorem proving graph grammars with attributes and negative application conditions
- Combining refinement and signal-temporal logic for biological systems
- Possible values: exploring a concept for concurrency
- Efficient symbolic computation of process expressions
- Semantics, calculi, and analysis for object-oriented specifications
- Consistency-preserving refactoring of refinement structures in Event-B models
- Satisfiability in composition-nominative logics
- Preservation of probabilistic information flow under refinement
- Formal specification method for systems automation
- Predicate diagrams for the verification of real-time systems
- Responsiveness and stable revivals
- Interactive tool support for CSP \(\parallel\) B consistency checking
- Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
- Specification and verification challenges for sequential object-oriented programs
- Automated reasoning with restricted intensional sets
- scientific article; zbMATH DE number 1615249 (Why is no real title available?)
- An extendible language for database schema refinement transformations
- B: Towards zero defect software
- From Sets to Bits in Coq
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Set-theoretic models of computations
- Pliant modalities in hybrid Event-B
- From predicates to programs: the semantics of a method language
- Domain-specific semantics and data refinement of object models
- Generic tools via general refinement
- rCOS: defining meanings of component-based software architectures
- Unifying theories of programming in Isabelle
- A new roadmap for linking theories of programming
- Proving Quicksort Correct in Event-B
- How to brew-up a refinement ordering
- Directed Model Checking for B: An Evaluation and New Techniques
- Specification of a localization component driven by a goal-based approach: some lessons we learned
- A formal framework for specifying and analyzing logs as electronic evidence
- Concurrent abstract state machines
- Patterns for refinement automation
- A refinement methodology for object-oriented programs
- Elements of B-method formalization
- Verifying B proof rules using deep embedding and automated theorem proving
- ASM-based formal design of an adaptivity component for a cloud system
- Modelling timed reactive systems from natural-language requirements
- Soundly proving B method formulæ using typed sequent calculus
- The subject-oriented approach to software design and the abstract state machines method
- Integrating simplex with tableaux
- Why Would You Trust B?
- iRho: an imperative rewriting calculus
- On the Purpose of Event-B Proof Obligations
- Generating Tests from B Specifications and Test Purposes
- A Practical Single Refinement Method for B
- The Composition of Event-B Models
- Modelling Attacker’s Knowledge for Cascade Cryptographic Protocols
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- On Automating the Calculus of Relations
- Efficient Well-Definedness Checking
- Fixpoints and search in PVS
- Modeling in Event B. System and software engineering.
- Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B
- Unifying Sets and Programs via Dependent Types
- Modelling of Complex Software Systems: A Reasoned Overview
- Incremental System Modelling in Event-B
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Unifying sets and programs via dependent types
- scientific article; zbMATH DE number 1258883 (Why is no real title available?)
- A functional framework for agent-based models of exchange
- Verification of distributed systems with local-global predicates
- Mechanised support for sound refinement tactics
- Compositional noninterference from first principles
- Experiments in program verification using Event-B
- 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
- JCML: A specification language for the runtime verification of Java card programs
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)
