Abstract is missing.
- SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside MicrosoftThomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani. 1-20 [doi]
- Design Verification for Control EngineeringRichard J. Boulton, Hanne Gottliebsen, Ruth Hardy, Tom Kelsey, Ursula Martin. 21-35 [doi]
- Integrating Model Checking and Theorem Proving in a Reflective Functional LanguageThomas F. Melham. 36-39 [doi]
- A Tutorial Introduction to Designs in Unifying Theories of ProgrammingJim Woodcock, Ana Cavalcanti. 40-66 [doi]
- An Integration of Program Analysis and Automated Theorem ProvingBill J. Ellis, Andrew Ireland. 67-86 [doi]
- Verifying Controlled ComponentsSteve Schneider, Helen Treharne. 87-107 [doi]
- Efficient CSP::Z:: Data AbstractionAdalberto Farias, Alexandre Mota, Augusto Sampaio. 108-127 [doi]
- State/Event-Based Software Model CheckingSagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha. 128-147 [doi]
- Formalising Behaviour Trees with CSPKirsten Winter. 148-167 [doi]
- UML to B: Formal Verification of Object-Oriented ModelsKevin Lano, David Clark, Kelly Androutsopoulos. 187-206 [doi]
- Software Verification with Integrated Data Type Refinement for Integer ArithmeticBernhard Beckert, Steffen Schlager. 207-226 [doi]
- Constituent Elements of a Correctness-Preserving UML Design ApproachTiberiu Seceleanu, Juha Plosila. 227-246 [doi]
- Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality AssumptionXu Wang, A. W. Roscoe, Ranko Lazic. 247-266 [doi]
- Linking CSP-OZ with UML and Java: A Case StudyMichael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim. 267-286 [doi]
- Object-Oriented Modelling with High-Level Modular Petri NetsCécile Bui Thanh, Hanna Klaudel. 287-306 [doi]
- Specification and Verification of Synchronizing Concurrent ObjectsGabriel Ciobanu, Dorel Lucanu. 307-327 [doi]
- Understanding Object-Z Operations as Generalised SubstitutionsSteve Dunne. 328-342 [doi]
- Embeddings of Hybrid Automata in Process AlgebraTim A. C. Willemse. 343-362 [doi]
- An Optimal Approach to Hardware/Software Partitioning for Synchronous ModelGeguang Pu, Dang Van Hung, Jifeng He, Wang Yi. 363-381 [doi]
- A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed ModelsAna Fernández Vilas, José J. Pazos Arias, Rebeca P. Díaz Redondo, Alberto Gil-Solla, Jorge García Duque. 382-401 [doi]
- Integrating Temporal LogicsYifeng Chen, Zhiming Liu. 402-420 [doi]
- Integration of Specification Languages Using ViewpointsMarius C. Bujorianu. 421-440 [doi]
- Integrating Formal Methods by Unifying AbstractionsRaymond T. Boute. 441-460 [doi]
- Formally Justifying User-Centred Design Rules: A Case Study on Post-completion ErrorsPaul Curzon, Ann Blandford. 461-480 [doi]
- Using UML Sequence Diagrams as the Basis for a Formal Test Description LanguageSimon Pickin, Jean-Marc Jézéquel. 481-500 [doi]
- Viewpoint-Based Testing of Concurrent ComponentsLuke Wildman, Roger Duke, Paul A. Strooper. 501-520 [doi]
- A Method for Compiling and Executing Expressive AssertionsFrancisco José Galán Morillo, José Miguel Cañete Valdeón. 521-540 [doi]