Skip past navigation NASA Langley Formal Methods

LFM 2008 > schedule
NASA Langley Research Center
The Sixth NASA Langley Formal Methods Workshop

April 30 - May 2, 2008

Timetable:

Wednesday, April 30
8:00-9:00
Registration
Session 1: Logic Into Practice
9:00-9:15   Kristin Y. Rozier (NASA LaRC)
  Welcome
9:15-9:45  Ricky W. Butler
 NASA Langley's Formal Methods Research in Support of the Next Generation Air Transportation System
9:45-10:45  Keynote Speaker: Moshe Y. Vardi
 From Philosophical to Industrial Logics
10:45-11:15
Coffee
Session Chair: Benedetto L. Di Vito    
11:15-11:45  Alessandro Cimatti, Marco Roveri, Angelo Susi, and Stefano Tonetta
 From Informal Safety-Critical Requirements to Property-Driven Formal Validation
11:45-12:15  Gopal Gupta
 Verification and Planning based on Coinductive Logic Programming
12:15-12:30  Ajitha Rajan, Mats Heimdahl, and Kurt Woodham
 Assessing Requirements Quality Through Requirements Coverage
12:30-14:00
Lunch
Session 2: Verification Under Constraints
Session Chair: Mahyar R. Malekpour    
14:00-14:30  Sudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Serbanuta, and Gheorghe Stefanescu
 Monitoring IVHM Systems using a Monitor-Oriented Programming Framework
14:30-15:00  Olga Brukman and Shlomi Dolev
 Self-* Programming: Run-Time Parallel Control Search for Reflection Box
15:00-15:30  William Gardner
 Getting Somewhat Formal with CSP and C++
15:30-16:15
Tea
Session Chair: Jeffrey M. Maddalon    
16:15-16:45  Borzoo Bonakdarpour and Sandeep Kulkarni
 Challenges and Demands on Automated Software Revision
16:45-17:00  Jorge Navas, Mario Mendez-Lojo, and Manuel Hermenegildo
 Safe Upper-bounds Inference of Energy Consumption for Java Bytecode Applications
17:00-17:15  John Paul, Nadya Kuzmina, Ruben Gamboa, and James Caldwell
 Toward a Formal Evaluation of Refactorings
Session Chair: Kristin Y. Rozier    
17:30-18:00  
 Relocation to the Virginia Air & Space Center (VaSC) via NASA buses
18:30-19:30  Keynote Speaker: Amy R. Pritchett
 Dinner Talk: The Nation's Needs in Aviation Formal Methods
19:45-22:00  VaSC Tour Guide
 Museum Tour followed by Museum Exploration

Thursday, May 1
Session 3: Certification and Practical Formal Methods
Session Chair: Paul S. Miner    
9:00-10:00  Keynote Speaker: John Rushby
 Formal Methods and Certification
10:00-10:30  Ewen Denney
 Certifying Auto-generated Flight Code
10:30-11:00
Coffee
11:00-11:30  Eduardo Rafael López Ruiz, Yves Ledru, and Michel Lemoine
 Aeronautical Regulations Should Be Rigorously Developed Too!
11:30-12:00  David Barton
 Use of Intelligent Assistants in Practical Theorem Proving
12:00-12:30  Arie Gurfinkel and Sagar Chaki
 Combining Predicate and Numeric Abstraction for Software Model Checking
12:30-14:00
Lunch
Session 4: Component-Based Verification
Session Chair: Radu I. Siminiceanu    
14:00-14:30  Mary Ann Malloy
 Reuse versus Reinvention: How will Formal Methods Deal with Composable Systems?
14:30-15:00  Panagiotis Manolios
 Automating System Assembly of Aerospace Systems
15:00-15:30  Sergey Tverdyshev and Andrey Shadrin
 Formal Verification of Gate-Level Computer Systems
15:30-16:00
Tea
16:00-16:30  Gregory Kulczycki and Amrinder Singh
 Proving Correctness for Pointer Programs in a Verifying Compiler
16:30-16:45  Matthew L. Bolton and Ellen J. Bass
 Formal Modeling of Erroneous Human Behavior and its Implications for Model Checking
16:45-17:00  Fernando Alegre and Eric Feron
 A Framework for Stability Analysis of Control Systems Software at the Source Code Level
17:00-17:15  John Carter
 Mise en Scene : A Scenario-Based Medium Supporting Formal Software Development

Friday, May 2
Session 5: The Future of Tools for Verification
Session Chair: Ricky W. Butler    
9:00-10:00  Keynote Speaker: Gerard J. Holzmann
 On Limits
10:00-10:30  Bruno Dutertre
 An Update on Yices
10:30-11:00
Coffee
11:00-11:30  Florent Kirchner
 Distributing Formal Verification: The Evidential Tool Bus
11:30-12:00  Lee Pike
 Model Checking for the Practical Verificationist: A User's Perspective on SAL
12:00-12:30  Alex Tsow
 An Overview of Starfish: A Table-Centric Tool for Interactive Synthesis
12:30-14:00
End of LFM 2008 / Lunch
[Top]

 

Skip past navigation  

Curator and Responsible NASA Official: Kristin Y. Rozier
LaRC Privacy Statement
last modified: January 17, 2008