Program (pdf)
| Day 1: April 13, 2010 (Tuesday) | 8:00 - 5:30 |
| Day 2: April 14, 2010 (Wednesday) | 8:30 - 5:30 |
| Day 3: April 15, 2010 (Thursday) | 9:00 - 12:30 |
DAY 1: April 13, 2010 (Tuesday)
8:00 - 8:45 Registration 8:45 - 9:00 Opening- John Kelly (NASA)
- Guillaume Brat (NASA). Verification and Validation of Flight-Critical Systems
- Sagar Chaki and Arie Gurfinkel. Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications
- Sarah Thompson, Guillaume Brat and Arnaud Venet. Software Model Checking of ARINC-653 Flight Code with MCP
- Xiaowan Huang, Anu Singh and Scott A. Smolka. Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol
- Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene. Automatic Review of Abstract State Machines by Meta Property Verification
- Andreas Bollin. Slice-based Formal Specification Measures - Mapping Coupling and Cohesion Measures to Formal Z
- Xiang Fu and Chung-Chih Li. Modeling Regular Replacement for String Constraint Solving
- Eduardo Rafael López Ruiz and Michel Lemoine. Can Regulatory Bodies Expect Efficient Help from Formal Methods?
- Petra Price and Greg Turgeon. Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking
- Sanaz Yeganefard, Michael Butler and Abdolbaghi Rezazadeh. Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B
DAY 2: April 14, 2010 (Wednesday)
8:30 - 9:00 Registration 9:00 - 10:00 Invited Talk (Chair: Ricky Butler)- John Harrison (Intel). Formal Methods at Intel - An Overview
- Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, Anthony Narkawicz and Gilles Dowek. How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project
- Concetta Pilotto and Jerome White. Verification of Faulty Message Passing Systems with Continuous State Space in PVS
- Dominic Richards and David Lester. A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem Prover
- Pritam Roy and Natarajan Shankar. SimCheck: An Expressive Type System for Simulink
- Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent Proofs of Numerical Programs
- Xiang Yin and John Knight. Formal Verification of Large Software Systems
- Nestor Cataño and Radu Siminiceanu. A Machine-Checked Proof of A State-Space Construction Algorithm
- Srinivas Nedunuri, Douglas R. Smith and William R. Cook. Synthesis of Greedy Algorithms Using Dominance Relations
- Yang Zhao and Gianfranco Ciardo. Symbolic Computation of Strongly Connected Components Using Saturation
DAY 3: April 15, 2010 (Thursday)
9:00 - 10:00 Invited Talk (Chair: César Muñoz)- Nikolaj Bjørner (Microsoft). Decision Engines for Software Analysis using Satisfiability Modulo Theories Solvers
- Erik Endres, Christian Müller, Andrey Shadrin and Sergey Tverdyshev. Towards the Formal Verification of a Distributed Real-Time Automotive System
- Viet Yen Nguyen, Thomas Noll and Max Odenbrett. Slicing AADL Specifications for Model Checking
- Pierre Roux and Radu Siminiceanu. Model Checking with Edge-valued Decision Diagrams
- Christian Saad and Bernhard Bauer. Data-flow Based Model Analysis
- Lehilton L. C. Pedrosa and Arnaldo V. Moura. A New Method for Incremental Testing of Finite State Machines
- Matt Staats, Michael Whalen, Ajitha Rajan and Mats Heimdahl. Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness