The following pages link to The B-Book (Q4208552):
Displaying 50 items.
- Set-Theoretic Models of Computations (Q2842623) (← links)
- Pliant Modalities in Hybrid Event-B (Q2842625) (← links)
- From predicates to programs: the semantics of a method language (Q2870332) (← links)
- Domain-specific semantics and data refinement of object models (Q2873615) (← links)
- Generic tools via general refinement (Q2873690) (← links)
- rCOS: Defining Meanings of Component-Based Software Architectures (Q2948228) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- A New Roadmap for Linking Theories of Programming (Q2971173) (← links)
- Proving Quicksort Correct in Event-B (Q2994490) (← links)
- How to Brew-up a Refinement Ordering (Q2994493) (← links)
- Directed Model Checking for B: An Evaluation and New Techniques (Q2999306) (← links)
- Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned (Q2999320) (← links)
- A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence (Q2999322) (← links)
- Patterns for Refinement Automation (Q3066119) (← links)
- A Refinement Methodology for Object-Oriented Programs (Q3067544) (← links)
- Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (Q3095242) (← links)
- Soundly Proving B Method Formulæ Using Typed Sequent Calculus (Q3179401) (← links)
- The Subject-Oriented Approach to Software Design and the Abstract State Machines Method (Q3223998) (← links)
- Integrating Simplex with Tableaux (Q3455763) (← links)
- Why Would You Trust B? (Q3498474) (← links)
- iRho: an imperative rewriting calculus (Q3520144) (← links)
- On the Purpose of Event-B Proof Obligations (Q3535369) (← links)
- Generating Tests from B Specifications and Test Purposes (Q3535370) (← links)
- A Practical Single Refinement Method for B (Q3535376) (← links)
- The Composition of Event-B Models (Q3535377) (← links)
- Modelling Attacker’s Knowledge for Cascade Cryptographic Protocols (Q3535379) (← links)
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification (Q3535380) (← links)
- On Automating the Calculus of Relations (Q3541686) (← links)
- Efficient Well-Definedness Checking (Q3541692) (← links)
- Fixpoints and Search in PVS (Q3558967) (← links)
- Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B (Q3605463) (← links)
- Unifying Sets and Programs via Dependent Types (Q3605541) (← links)
- Modelling of Complex Software Systems: A Reasoned Overview (Q3613056) (← links)
- Incremental System Modelling in Event-B (Q3638993) (← links)
- Combinations of Theories for Decidable Fragments of First-Order Logic (Q3655205) (← links)
- Adding partial functions to Constraint Logic Programming with sets (Q4593005) (← links)
- A case study in the mechanical verification of fault tolerance (Q4783363) (← links)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs (Q4916225) (← links)
- A Conceptual and Formal Framework for the Integration of Data Type and Process Modeling Techniques (Q4921549) (← links)
- A Behavioural Theory of Recursive Algorithms (Q4988914) (← links)
- Action systems in incremental and aspect-oriented modeling (Q5138491) (← links)
- Automatic Verification of Bossa Scheduler Properties (Q5178992) (← links)
- Incremental Parametric Development of Greedy Algorithms (Q5178994) (← links)
- Specification and Runtime Verification of Java Card Programs (Q5179352) (← links)
- Verified Compilation and the B Method: A Proposal and a First Appraisal (Q5179355) (← links)
- Combining Decision Procedures by (Model-)Equality Propagation (Q5179357) (← links)
- Compositionality: Ontology and Mereology of Domains (Q5187818) (← links)
- Model-Based Testing for Functional and Security Test Generation (Q5253584) (← links)
- Panelist position statement: reasoning about the design of programs (Q5301853) (← links)
- Refinement-Based Verification of Interactive Real-Time Systems (Q5403466) (← links)
