| Little Engines of Proof / Natarajan Shankar |
| Automated Boundary Testing from Z and B / Bruno Legeard ; Fabien Peureux ; Mark Utting |
| Improvements in Coverability Analysis / Gil Ratsaby ; Baruch Sterin ; Shmuel Ur |
| Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study / Juan C. Burguillo-Rial ; Manuel J. Fernandez-Iglesias ; Francisco J. González-Castaño ; MartÃn Llamas-Nistal |
| UniTesK Test Suite Architecture / Igor B. Bourdonov ; Alexander S. Kossatchev ; Victor V. Kuliamin ; Alexander K. Petrenko |
| Hoare Logicfor NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited / David von Oheimb ; Tobias Nipkow |
| Do Not Read This / Juan C. Bicarregui |
| Safeness of Make-Based Incremental Recompilation / Niels Jørgensen |
| An AlgorithmicApproach to Design Exploration / Sharon Barner ; Shoham Ben-David ; Anna Gringauze ; Yaron Wolfsthal |
| Verifying Erlang Code: A Resource Locker Case-Study / Alexandre Mota ; Paulo Borba ; Augusto Sampaio ; Thomas Arts ; Clara Benac Earle ; John Derrick |
| Towards an Integrated Model Checker for Railway Signalling Data / Michael Huber ; Steve King |
| Correctness by Construction: Integrating Formality into a Commercial Development Process / Anthony Hall |
| VAlloy - Virtual Functions Meet a Relational Language / Darko Marinov ; Sarfraz Khurshid |
| Verification Using Test Generation Techniques / Vlad Rusu |
| Formal Specification and Static Checking of GemplusÆ Electronic Purse Using ESC/Java / Nestor Catano ; Marieke Huisman |
| Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods / Ludovic Casset |
| Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation / Michael Backes ; Christian Jacobi ; Birgit Pfitzmann |
| Interference Analysis for Dependable Systems Using Refinement and Abstraction / Claus Pahl |
| The Formal Classification and Verification of SimpsonÆs 4-Slot Asynchronous Communication Mechanism / N. Henderson ; S.E. Paynter |
| Timing Analysis of Assembler Code Control-Flow Paths / C.J. Fidge |
| Towards OCL/RT / MarÃa Victoria Cengarle ; Alexander Knapp |
| On Combining Functional Verification and Performance Evaluation Using CADP / Hubert Garavel ; Holger Hermanns |
| The Next 700 Synthesis Calculi / David Basin |
| Synthesizing Certified Code / Michael Whalen ; Johann Schumann ; Bernd Fischer |
| Refinement in Circus / Jim Woodcock ; Ana Cavalcanti |
| Forward Simulation for Data Refinement of Classes / David A. Naumann |
| A Formal Basis for a Program Compilation Proof Tool / Luke Wildman |
| Property Dependent Abstraction of Control Structure for Software Verification / Thomas Firley ; Ursula Goltz |
| Closing Open SDL-Systems for Model Checking with DTSpin / Natalia Ioustinova ; Natalia Sidorova ; Martin Steffen |
| A Generalised Sweep-Line Method for Safety Properties / Lars Michael Kristensen ; Thomas Mailund |
| Supplementing a UML Development Process with B / Helen Treharne |
| SemanticWeb for Extending and Linking Formalisms / Jin Song Dong ; Jing Sun ; Hai Wang |
| A Language for Describing Wireless Mobile Applications with DynamicEstablishment of Multi-way Synchronization Channels / Takaaki Umedu ; Yoshiki Terashima ; Keiichi Yasumoto ; Akio Nakata ; Teruo Higashino ; Kenichi Taniguchi |
| Author Index |
| Little Engines of Proof / Natarajan Shankar |
| Automated Boundary Testing from Z and B / Bruno Legeard ; Fabien Peureux ; Mark Utting |
| Improvements in Coverability Analysis / Gil Ratsaby ; Baruch Sterin ; Shmuel Ur |
図書
ＥＢ
