Abstract is missing.
- Automatic Review of Abstract State Machines by Meta Property VerificationPaolo Arcaini, Angelo Gargantini, Elvinia Riccobene. 4-13
- Hardware-independent Proofs of Numerical ProgramsSylvie Boldo, Thi Minh Tuyen Nguyen. 14-23
- Slice-based Formal Specification Measures - Mapping Coupling and Cohesion Measures to Formal ZAndreas Bollin. 24-33
- How Formal Methods Impels Discovery: A Short History of an Air Traffic Management ProjectRicky W. Butler, George Hagen, Jeffrey Maddalon, César A. Muñoz, Anthony Narkawicz, Gilles Dowek. 34-46
- A Machine-Checked Proof of A State-Space Construction AlgorithmNéstor Cataño, Radu I. Siminiceanu. 47-56
- Automated Assume-Guarantee Reasoning for Omega-Regular Systems and SpecificationsSagar Chaki, Arie Gurfinkel. 57-66
- Modeling Regular Replacement for String Constraint SolvingXiang Fu, Chung-Chih Li. 67-76
- Using Integer Clocks to Verify the Timing-Sync Sensor Network ProtocolXiaowan Huang, Anu Singh, Scott A. Smolka. 77-86
- Can Regulatory Bodies Expect Efficient Help from Formal Methods?Eduardo Rafael López Ruiz, Michel Lemoine. 87-96
- Synthesis of Greedy Algorithms Using Dominance RelationsSrinivas Nedunuri, Douglas R. Smith, William R. Cook. 97-108
- A New Method for Incremental Testing of Finite State MachinesLehilton L. C. Pedrosa, Arnaldo V. Moura. 109-118
- Verification of Faulty Message Passing Systems with Continuous State Space in PVSConcetta Pilotto, Jerome White. 119-128
- Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model CheckingPetra Price, Greg Turgeon. 129-138
- A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem ProverDominic Richards, David R. Lester. 139-148
- SimCheck: An Expressive Type System for SimulinkPritam Roy, Natarajan Shankar. 149-160
- Coverage Metrics for Requirements-Based Testing: Evaluation of EffectivenessMatt Staats, Michael W. Whalen, Ajitha Rajan, Mats Per Erik Heimdahl. 161-170
- Software Model Checking of ARINC-653 Flight Code with MCPSarah Thompson, Guillaume P. Brat, Arnaud Venet. 171-181
- Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-BSanaz Yeganefard, Michael Butler, Abdolbaghi Rezazadeh. 182-191
- Formal Verification of Large Software SystemsXiang Yin, John C. Knight. 192-201
- Symbolic Computation of Strongly Connected Components Using SaturationYang Zhao, Gianfranco Ciardo. 202-211
- Towards the Formal Verification of a Distributed Real-Time Automotive SystemErik Endres, Christian Müller, Andrey Shadrin, Sergey Tverdyshev. 212-216
- Slicing AADL Specifications for Model CheckingViet Yen Nguyen, Thomas Noll, Max Odenbrett. 217-221
- Model Checking with Edge-valued Decision DiagramsPierre Roux, Radu Siminiceanu. 222-226
- Data-flow Based Model AnalysisChristian Saad, Bernhard Bauer. 227-231