Abstract is missing.
- Attacking Large Industrial Code with Bi-abductive InferenceDino Distefano. 1-8 [doi]
- On a Uniform Framework for the Definition of Stochastic Process LanguagesRocco De Nicola, Diego Latella, Michele Loreti, Mieke Massink. 9-25 [doi]
- Applying a Formal Method in Industry: A 15-Year TrajectoryThierry Lecomte. 26-34 [doi]
- What s in Common between Test, Model Checking, and Decision Procedures?Kenneth L. McMillan. 35-36 [doi]
- Verifying Cryptographic Software Correctness with Respect to Reference ImplementationsJosé Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira. 37-52 [doi]
- Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics SoftwareDavid Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal, Franck Védrine. 53-69 [doi]
- Dynamic State Space Partitioning for External Memory Model CheckingSami Evangelista, Lars Michael Kristensen. 70-85 [doi]
- Compositional Verification of a Communication Protocol for a Remotely Operated VehicleAlwyn Goodloe, César A. Muñoz. 86-101 [doi]
- Modeling Concurrent Systems with Shared ResourcesÃngel Herranz-Nieva, Julio Mariño, Manuel Carro, Juan José Moreno-Navarro. 102-116 [doi]
- Platform-Specific Restrictions on Concurrency in Model Checking of Java ProgramsPavel Parizek, Tomás Kalibera. 117-132 [doi]
- Formal Analysis of Non-determinism in Verilog Cell Library Simulation ModelsMatthias Raffelsieper, Mohammad Reza Mousavi, Jan-Willem Roorda, Chris W. H. Strolenberg, Hans Zantema. 133-148 [doi]
- Preemption AbstractionErik Schierboom, Alejandro Tamalet, Hendrik Tews, Marko C. J. D. van Eekelen, Sjaak Smetsers. 149-164 [doi]
- A Rigorous Methodology for Composing ServicesKenneth J. Turner, Koon Leai Larry Tan. 165-180 [doi]
- A Certified Implementation on Top of the Java Virtual MachineJavier de Dios, Ricardo Peña-MarÃ. 181-196 [doi]
- Formal Development for Railway Signaling Using Commercial ToolsAlessio Ferrari, Alessandro Fantechi, Stefano Bacherini, Niccolò Zingoni. 197-198 [doi]
- Integrated Formal Approach for Qualified Critical Embedded Code GeneratorNassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai. 199-201 [doi]
- Visualising Event-B Models with B-Motion StudioLukas Ladenberger, Jens Bendisposto, Michael Leuschel. 202-204 [doi]
- Behavioural Analysis of an I:::2:::C Linux DriverDragan Bosnacki, Aad Mathijssen, Yaroslav S. Usenko. 205-206 [doi]
- Model-Based Testing of Electronic PassportsWojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans, Ronny Wichers Schreur. 207-209 [doi]
- Developing a Decision Support Tool for Dam Management with SPINMarÃa-del-Mar Gallardo, Pedro Merino, Laura Panizo, Antonio Linares. 210-212 [doi]