NASA Logo, National Aeronautics and Space Administration

NFM'09 PROGRAM

DAY 1: April 6, 2009 (Monday)


8 - 8.30: Registration


8.30 - 9: Opening


9 - 10: Invited Talk

(Chair: Corina Pasareanu)

  • Ed Clarke (CMU, Turing Award 2007). Model Checking -- My 27-year Quest to Overcome the State Explosion Problem

10 - 10.30: Break


10.30 - 12.30: Model Checking: Techniques and Applications

(Chair: Bernhard Steffen)

  • Matthew Bolton and Ellen Bass. Building a Formal Model of a Human-interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering

  • Emil Vassev and Mike Hinchey. Model Checking for Autonomic Systems Specified with ASSL
  • Yi Wang and Tetsuo Tamai. A Game-Theoretic Approach to Branching Time Abstract-Check-Refine Process
  • Sagar Chaki and James Ivers. Software Model Checking without Source Code

12.30 - 14: Lunch


14 - 15: Invited Talk

(Chair: Mike Lowry)

  • Bill Othon (NASA JSC). Applying Formal Methods to NASA Projects: Transition from Research to Practice

15- 15.30: Break


15.30 - 16.30: Symbolic Execution and Testing

(Chair: John Penix)

  • Suzette Person and Matthew Dwyer. Generalized Abstract Symbolic Summaries for Differencing Heap-manipulating Programs

  • Mitsuo Takaki, Diego Cavalcanti, Rohit Gheyi, Juliano Iyoda, Marcelo d'Amorim and Ricardo Prudencio. A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing

DAY 2: April 7, 2009 (Tuesday)


9 - 10: Invited Talk

(Chair: Dimitra Giannakoupoulou)

  • Leslie Lamport (MSR). TLA+: Whence, Wherefore, and Whither

10 - 10.30: Break


10.30 - 12.30 Design and Specification

(Chair: Matt Dwyer)

  • Tiziana Margaria, Marco Bakera, Christian Wagner, Emil Vassev, Michael Hinchey and Bernhard Steffen. Component-Oriented Behavior Extraction for Autonomic System Design
  • Jonathan Nicholson, Epameinondas Gasparis, Amnon Eden and Rick Kazman. Automated Verification of Design Patterns with LePUS3
  • Yann Glouche, Jean-Pierre Talpin, Paul Le Guernic and Thierry Gautier. A module language for typing by contracts

  • Benjamin Aziz, Alvaro Arenas, Juan Bicarregui, Christophe Ponsard and Philippe Massonet. From Goal-Oriented Requirements to Event-B Specifications

12.30 - 14: Lunch


14 - 15: Invited Talk

(Chair: Joe Coughlan)

  • Todd Farley (NASA Ames). Formal Methods Applications in Air Transportation

15 - 15.30: Break


15.30 - 16.30: Analysis: Evaluations and New Developments (Short Papers)

(Chair: Radu Siminiceanu)

  • Watcharin Leungwattanakit, Cyrille Valentin Artho, Masami Hagiya, Yoshinori Tanabe and Mitsuharu Yamamoto. Introduction of Virtualization Technology to Multi-Process Model Checking
  • David Cachera and David Pichardie. Comparing Techniques for Certified Static Analysis
  • Matt Staats. Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder

  • Karthick Jayaraman, David Harvison, Vijay Ganesh and Adam Kiezun. jFuzz: A Concolic Whitebox Fuzzer for Java

18.30 - 20: Banquet -- Michaels at Shoreline



DAY 3: April 8, 2009 (Wednesday)


9 - 10: Invited Talk

(Chair: Ewen Denney)

  • John O'Leary (Intel). Theorem Proving in Intel Hardware Design

10 - 10.30: Break


10.30 - 12.30: Deductive Verification

(Chair: Doug Smith)

  • Thomas Göthel and Sabine Glesner. Machine-Checkable Timed CSP

  • Marc Daumas, Erik Martin-Dorel, David Lester and Annick Truffert. Stochastic Formal Methods for Hybrid Systems
  • Manuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto and Bárbara Vieira. Deductive Verification of Cryptographic Software
  • Christine Choppy, Micaela Mayero and Laure Petrucci. Coloured Petri net re?nement speci?cation, and correctness proof with Coq

12.30 - 14: Lunch


14 - 15: Panel: Formal Methods meet NASA needs

(Chair: Mats Heimdahl)

  • Panelists: Byron Cook (Microsoft), Gabor Karsai (Vanderbilt U.), Mike Lowry (NASA Ames), John Robinson (NASA Ames)

15 - 15.30: Break


15.30 - 16.30: Modeling and Synthesis (Short Papers)

(Chair: Kristin Yvonne Rozier)

  • Alessio Ferrari, Alessandro Fantechi, Stefano Bacherini and Niccolo' Zingoni. Modeling Guidelines for Code Generation in the Railway Signaling Context

  • Srinivas Nedunuri, William Cook and Douglas Smith. Tactical Synthesis of Efficient Global Search Algorithms
  • Manuela Luminita Bujorianu and Marius Bujorianu. Towards Co-Engineering Communicating Autonomous Cyber-physical Systems
  • Juhan Ernits, Richard Dearden and Miles Pebody. Formal Methods for Automated Diagnosis of Autosub 6000

16:30: Closing NFM'09

First Gov logo
NASA Logo - nasa.gov