Abstract is missing.
- Little Engines of ProofNatarajan Shankar. 1-20 [doi]
- Automated Boundary Testing from Z and BBruno Legeard, Fabien Peureux, Mark Utting. 21-40 [doi]
- Improvements in Coverability AnalysisGil Ratsaby, Baruch Sterin, Shmuel Ur. 41-56 [doi]
- Heuristic-Driven Test Case Selection from Formal Specifications. A Case StudyJuan C. Burguillo-Rial, Manuel J. Fernández Iglesias, Francisco J. González-Castaño, Martín Llamas Nistal. 57-76 [doi]
- UniTesK Test Suite ArchitectureIgor B. Bourdonov, Alexander Kossatchev, Victor V. Kuliamin, Alexander K. Petrenko. 77-88 [doi]
- Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods RevisitedDavid von Oheimb, Tobias Nipkow. 89-105 [doi]
- Do Not Read ThisJuan Bicarregui. 106-125 [doi]
- Safeness of Make-Based Incremental RecompilationNiels Jørgensen. 126-145 [doi]
- An Algorithmic Approach to Design ExplorationSharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal. 146-162 [doi]
- Mechanical Abstraction of CSP::Z:: ProcessesAlexandre Mota, Paulo Borba, Augusto Sampaio. 163-183 [doi]
- Verifying Erlang Code: A Resource Locker Case-StudyThomas Arts, Clara Benac Earle, John Derrick. 184-203 [doi]
- Towards an Integrated Model Checker for Railway Signalling DataMichael Huber, Steve King. 204-223 [doi]
- Correctness by Construction: Integrating Formality into a Commercial Development ProcessAnthony Hall. 224-233 [doi]
- VAlloy - Virtual Functions Meet a Relational LanguageDarko Marinov, Sarfraz Khurshid. 234-251 [doi]
- Verification Using Test Generation TechniquesVlad Rusu. 252-271 [doi]
- Formal Specification and Static Checking of Gemplus Electronic Purse Using ESC/JavaNéstor Cataño, Marieke Huisman. 272-289 [doi]
- Development of an Embedded Verifier for Java Card Byte Code Using Formal MethodsLudovic Casset. 290-309 [doi]
- Deriving Cryptographically Sound Implementations Using Composition and Formally Verified BisimulationMichael Backes, Christian Jacobi 0002, Birgit Pfitzmann. 310-329 [doi]
- Interference Analysis for Dependable Systems Using Refinement and AbstractionClaus Pahl. 330-349 [doi]
- The Formal Classification and Verification of Simpson s 4-Slot Asynchronous Communication MechanismNeil Henderson, Stephen Paynter. 350-369 [doi]
- Timing Analysis of Assembler Code Control-Flow PathsColin J. Fidge. 370-389 [doi]
- Towards OCL/RTMaría Victoria Cengarle, Alexander Knapp. 390-409 [doi]
- On Combining Functional Verification and Performance Evaluation Using CADPHubert Garavel, Holger Hermanns. 410-429 [doi]
- The Next 700 Synthesis CalculiDavid A. Basin. 430 [doi]
- Synthesizing Certified CodeMichael W. Whalen, Johann Schumann, Bernd Fischer. 431-450 [doi]
- Refinement in CircusAugusto Sampaio, Jim Woodcock, Ana Cavalcanti. 451-470 [doi]
- Forward Simulation for Data Refinement of ClassesAna Cavalcanti, David A. Naumann. 471-490 [doi]
- A Formal Basis for a Program Compilation Proof ToolLuke Wildman. 491-510 [doi]
- Property Dependent Abstraction of Control Structure for Software VerificationThomas Firley, Ursula Goltz. 511-530 [doi]
- Closing Open SDL-Systems for Model Checking with DTSpinNatalia Ioustinova, Natalia Sidorova, Martin Steffen. 531-548 [doi]
- A Generalised Sweep-Line Method for Safety PropertiesLars Michael Kristensen, Thomas Mailund. 549-567 [doi]
- Supplementing a UML Development Process with BHelen Treharne. 568-586 [doi]
- Semantic Web for Extending and Linking FormalismsJin Song Dong, Jing Sun, Hai H. Wang. 587-606 [doi]
- A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization ChannelsTakaaki Umedu, Yoshiki Terashima, Keiichi Yasumoto, Akio Nakata, Teruo Higashino, Kenichi Taniguchi. 607-624 [doi]