Directed Model Checking for B: An Evaluation and New Techniques | p. 1 |
Midlet Navigation Graphs in JML | p. 17 |
Runtime Verification for Generic Classes with ConGu2 | p. 33 |
A High-Level Language for Modeling Algorithms and Their Properties | p. 49 |
A Formal Environment Model for Multi-Agent Systems | p. 64 |
A Modal Interface Theory with Data Constraints | p. 80 |
Synchronizing Model and Program Refactoring | p. 96 |
A Type-Theoretic Framework for Certified Model Transformations | p. 112 |
Simulating Truly Concurrent CSP | p. 128 |
Statistical Verification of Probabilistic Properties with Unbounded Until | p. 144 |
Reasoning about Assignments in Recursive Data Structures | p. 161 |
Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned | p. 177 |
A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence | p. 194 |
Formal Development of a Cardiac Pacemaker: From Specification to Code | p. 210 |
A Decision Procedure for Bisimilarity of Generalized Regular Expressions | p. 226 |
Normalization of Linear Horn Clauses | p. 242 |
A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs | p. 258 |
Automating Refinement of Circus Programs | p. 274 |
Author Index | p. 291 |
Table of Contents provided by Ingram. All Rights Reserved. |
The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.
The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.