The B-Book

DOI10.1017/CBO9780511624162zbMath0915.68015OpenAlexW4254354208MaRDI QIDQ4208552

Publication date: 6 September 1998

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

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

Related Items (only showing first 100 items - show all)

An Automation-Friendly Set Theory for the B Method ⋮ A case study in the mechanical verification of fault tolerance ⋮ Integrating Simplex with Tableaux ⋮ Soundly Proving B Method Formulæ Using Typed Sequent Calculus ⋮ Panelist position statement: reasoning about the design of programs ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ Unifying Theories of Programming in Isabelle ⋮ The Subject-Oriented Approach to Software Design and the Abstract State Machines Method ⋮ Why Would You Trust B? ⋮ Query-driven verification of data integration in the RDF data model ⋮ Adding partial functions to Constraint Logic Programming with sets ⋮ An automatically verified prototype of the Android permissions system ⋮ Trace preservation in B and Event-B refinements ⋮ Verification-Led Smart Contracts ⋮ Toward a theory of program repair ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ iRho: an imperative rewriting calculus ⋮ A New Roadmap for Linking Theories of Programming ⋮ 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 ⋮ Action systems in incremental and aspect-oriented modeling ⋮ 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 ⋮ Fixpoints and Search in PVS ⋮ Refinement-Based Verification of Interactive Real-Time Systems ⋮ Linking Event-B and Concurrent Object-Oriented Programs ⋮ Experimenting Formal Proofs of Petri Nets Refinements ⋮ General Refinement, Part One: Interfaces, Determinism and Special Refinement ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ A Conceptual and Formal Framework for the Integration of Data Type and Process Modeling Techniques ⋮ Automatic Verification of Bossa Scheduler Properties ⋮ Incremental Parametric Development of Greedy Algorithms ⋮ Specification and Runtime Verification of Java Card Programs ⋮ Verified Compilation and the B Method: A Proposal and a First Appraisal ⋮ Combining Decision Procedures by (Model-)Equality Propagation ⋮ Compositionality: Ontology and Mereology of Domains ⋮ Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B ⋮ Unifying Sets and Programs via Dependent Types ⋮ Patterns for Refinement Automation ⋮ Modelling of Complex Software Systems: A Reasoned Overview ⋮ A Refinement Methodology for Object-Oriented Programs ⋮ Finding Counter Examples in Induction Proofs ⋮ Incremental System Modelling in Event-B ⋮ Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving ⋮ A Behavioural Theory of Recursive Algorithms ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ Pliant Modalities in Hybrid Event-B ⋮ Model-Based Testing for Functional and Security Test Generation ⋮ From Predicates to Programs: The Semantics of a Method Language ⋮ Domain-specific Semantics and Data Refinement of Object Models ⋮ Generic Tools via General Refinement ⋮ Discussion on: ``Formal specification method for systems automation ⋮ Theorem proving graph grammars with attributes and negative application conditions ⋮ Specification and refinement of mobile systems in MTLA and mobile UML ⋮ Components as coalgebras: the refinement dimension ⋮ An Event-B based approach for cloud composite services verification ⋮ Combining refinement and signal-temporal logic for biological systems ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ 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 ⋮ Invariant-driven specifications in Maude ⋮ Possible values: exploring a concept for concurrency ⋮ Concurrent abstract state machines ⋮ ASM-based formal design of an adaptivity component for a cloud system ⋮ Modelling timed reactive systems from natural-language requirements ⋮ Integrating formal specifications into applications: the ProB Java API ⋮ Tank monitoring: A pAMN case study ⋮ Transposing partial components--an exercise on coalgebraic refinement ⋮ 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 ⋮ Efficient symbolic computation of process expressions ⋮ Semantics, calculi, and analysis for object-oriented specifications ⋮ Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm ⋮ Unnamed Item ⋮ 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 ⋮ Verifying a signature architecture: a comparative case study ⋮ Splitting atoms safely ⋮ Automated reasoning with restricted intensional sets ⋮ Consistency-preserving refactoring of refinement structures in Event-B models ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Unifying sets and programs via dependent types ⋮ Temporal-logic property preservation under Z refinement ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Security invariants in discrete transition systems ⋮ Integrating stochastic reasoning into Event-B development ⋮ A functional framework for agent-based models of exchange

This page was built for publication: The B-Book