| 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 | ||
Curator and Responsible NASA Official: Kristin Y. Rozier
LaRC Privacy Statement
last modified: January 17, 2008