Abstract is missing.
- Aspects and Formal MethodsShmuel Katz. 1-11 [doi]
- Getting Formal Verification into Design FlowArvind, Nirav Dave, Michael Katelman. 12-32 [doi]
- Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real SystemsDawson R. Engler. 33 [doi]
- Simulation, Orchestration and Logical ClocksDavid Kitchin, Evan Powell, Jayadev Misra. 34 [doi]
- CoVaC: Compiler Validation by Program Analysis of the Cross-ProductAnna Zaks, Amir Pnueli. 35-51 [doi]
- Lazy Behavioral SubtypingJohan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen. 52-67 [doi]
- Checking Well-Formedness of Pure-Method SpecificationsArsenii Rudich, Ádám Darvas, Peter Müller. 68-83 [doi]
- Verifying Dynamic Pointer-Manipulating ThreadsThomas Noll, Stefan Rieger. 84-99 [doi]
- Proofs and Refutations for Probabilistic RefinementA. K. McIver, C. C. Morgan, C. Gonzalia. 100-115 [doi]
- Assume-Guarantee Verification for Interface AutomataMichael Emmi, Dimitra Giannakopoulou, Corina S. Pasareanu. 116-131 [doi]
- Automated Verification of Dense-Time MTL Specifications Via Discrete-Time ApproximationCarlo A. Furia, Matteo Pradella, Matteo Rossi. 132-147 [doi]
- A Model Checking Language for Concurrent Value-Passing SystemsRadu Mateescu, Damien Thivolle. 148-164 [doi]
- Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified CodeHolger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn, Wolfgang Reif. 165-180 [doi]
- Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDMHugo Daniel Macedo, Peter Gorm Larsen, John S. Fitzgerald. 181-197 [doi]
- Industrial Use of Formal Methods for a High-Level Security EvaluationBoutheina Chetali, Quang Huy Nguyen. 198-213 [doi]
- Secret Ninja Formal MethodsJoseph R. Kiniry, Daniel M. Zimmerman. 214-228 [doi]
- Specification and Checking of Software Contracts for Conditional Information FlowTorben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David Greve. 229-245 [doi]
- JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong ValidityPatrice Chalin, Frédéric Rioux. 246-261 [doi]
- Provably Correct Runtime MonitoringIrem Aktug, Mads Dam, Dilian Gurov. 262-277 [doi]
- A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOSOlivier Ponsini, Wendelin Serwe. 278-293 [doi]
- A Rigorous Approach to Networking: TCP, from Implementation to Protocol to ServiceTom Ridge, Michael Norrish, Peter Sewell. 294-309 [doi]
- Constraint Prioritization for Efficient Analysis of Declarative ModelsEngin Uzuncaova, Sarfraz Khurshid. 310-325 [doi]
- Finding Minimal Unsatisfiable Cores of Declarative SpecificationsEmina Torlak, Felix Sheng-Ho Chang, Daniel Jackson. 326-341 [doi]
- Precise Interval Analysis vs. Parity GamesThomas Gawlitza, Helmut Seidl. 342-357 [doi]
- Introducing Objects through RefinementTim McComb, Graeme Smith. 358-373 [doi]
- Masking Faults While Providing Bounded-Time Phased RecoveryBorzoo Bonakdarpour, Sandeep S. Kulkarni. 374-389 [doi]
- Towards Consistent Specifications of Product FamiliesAlexander Harhurin, Judith Hartmann. 390-405 [doi]
- Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets DistributionScott Lintelman, Richard Robinson, Mingyan Li, Krishna Sampigethaya. 406-410 [doi]
- An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOSEric Verhulst, Gjalt G. de Jong, Vitaliy Mezhuyev. 411-418 [doi]
- Software Engineering with Formal Methods: Experiences with the Development of a Storm Surge Barrier Control SystemKlaas Wijbrans, Franc Buve, Robin Rijkers, Wouter Geurts. 419-424 [doi]
- Application of a Formal Specification Language in the Development of the Mobile FeliCa IC Chip Firmware for Embedding in Mobile PhoneTaro Kurita, Miki Chiba, Yasumasa Nakatsugawa. 425-429 [doi]
- Safe and Reliable Metro Platform Screen Doors Control/Command SystemsThierry Lecomte. 430-434 [doi]