Front matter
27-50
Little Engines of Proof
Natarajan Shankar
221-236
Automated Boundary Testing from Z and B
Bruno Legeard, Fabien Peureux and Mark Utting
91-102
Improvements in Coverability Analysis
Gil Ratsaby, Baruch Sterin and Shmuel Ur
141-148
Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study
Juan C. Burguillo-Rial, Manuel J. Fernández-Iglesias, Francisco J. González-Castaño and Martín Llamas-Nistal
121-152
UniTesK Test Suite Architecture
Igor B. Bourdonov, Alexander S. Kossatchev, Victor V. Kuliamin and Alexander K. Petrenko
37-49
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited
David von Oheimb and Tobias Nipkow
179-189
Do Not Read This
Juan C. Bicarregui
126-145
Safeness of Make-Based Incremental Recompilation
Niels Jørgensen
17-35
An Algorithmic Approach to Design Exploration
Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin and Yaron Wolfsthal
1-3
Mechanical Abstraction of CSP
Z
Processes
Alexandre Mota, Paulo Borba and Augusto Sampaio
191-220
Verifying Erlang Code: A Resource Locker Case-Study
Thomas Arts, Clara Benac Earle and John Derrick
204-223
Towards an Integrated Model Checker for Railway Signalling Data
Michael Huber and Steve King
139-157
Correctness by Construction: Integrating Formality into a Commercial Development Process
Anthony Hall
37-60
VAlloy — Virtual Functions Meet a Relational Language
Darko Marinov and Sarfraz Khurshid
51-79
Verification Using Test Generation Techniques
Vlad Rusu
272-289
Formal Specification and Static Checking of Gemplus’ Electronic Purse Using ESC/Java
Néstor Cataño and Marieke Huisman
27-35
Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods
Ludovic Casset
81-120
Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation
Michael Backes, Christian Jacobi and Birgit Pfitzmann
1-26
Interference Analysis for Dependable Systems Using Refinement and Abstraction
Claus Pahl
121-132
The Formal Classification and Verification of Simpson’s 4-Slot Asynchronous Communication Mechanism
N. Henderson and S. E. Paynter
159-165
Timing Analysis of Assembler Code Control-Flow Paths
C. J. Fidge
295-311
Towards OCL/RT
María Victoria Cengarle and Alexander Knapp
103-118
On Combining Functional Verification and Performance Evaluation Using CADP
Hubert Garavel and Holger Hermanns
61-76
The Next 700 Synthesis Calculi
David Basin
149-155
Synthesizing Certified Code
Michael Whalen, Johann Schumann and Bernd Fischer
1-15
Refinement in
Circus
Augusto Sampaio, Jim Woodcock and Ana Cavalcanti
133-140
Forward Simulation for Data Refinement of Classes
Ana Cavalcanti and David A. Naumann
153-189
A Formal Basis for a Program Compilation Proof Tool
Luke Wildman
231-242
Property Dependent Abstraction of Control Structure for Software Verification
Thomas Firley and Ursula Goltz
157-177
Closing Open SDL-Systems for Model Checking with DTSpin
Natalia Ioustinova, Natalia Sidorova and Martin Steffen
215-229
A Generalised Sweep-Line Method for Safety Properties
Lars Michael Kristensen and Thomas Mailund
119-137
Supplementing a UML Development Process with B
Helen Treharne
77-90
Semantic Web for Extending and Linking Formalisms
Jin Song Dong, Jing Sun and Hai Wang
5-25
A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels
Takaaki Umedu, Yoshiki Terashima, Keiichi Yasumoto, Akio Nakata and Teruo Higashino, et al.
Back matter