Schedule
Click here for a more printer-friendly PDF.
| Tue, June 7 | ||
| 8:00-8:15 | Check-in/Registration, Welcome and Opening Remarks | |
| 8:15-9:15 | Session: Keynote | |
| Using Formal Methods to Eliminate Exploitable Bugs | Kathleen Fisher | |
| 9:15-9:45 | Break | |
| 9:45-11:15 | Session: Requirements and Architectures | Chair: Darren Cofer |
| 9:45-10:15 | Temporal Logic Framework for Performance Analysis of Architectures of Systems | Ariane Piel, Jean Bourrely, St ephanie Lala, Sylvain Bertrand and Romain |
| 10:15-10:45 | On Implementing Real-time Specification Patterns Using Observers | John Backes, Michael Whalen, Andrew Gacek and John Komp |
| 10:45-11:00 | Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems | Devesh Bhatt, Arunabh Chattopadhyay, Wenchao Li, David Oglesby, Sam Owre and Natarajan Shankar |
| 11:00-11:15 | ARSENAL: Automatic Requirements Specification Extraction from Natural Language | Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar and Wilfried Steiner |
| 11:15-12:45 | Lunch | |
| 12:45-3:00 | Session: Testing and Run-time Enforcement | Chair: Zvonimir Rakamaric |
| 12:45-1:15 | Assisted Coverage Closure | Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening, Peter Schrammel and Michael Tautschnig |
| 1:15-1:45 | Synthesizing Runtime Enforcer of Safety Properties under Burst Error | Meng Wu, Haibo Zeng and Chao Wang |
| 1:45-2:00 | Break | |
| 2:00-2:30 | Compositional Runtime Enforcement | Srinivas Pinisetty and Stavros Tripakis |
| 2:30-2:45 | Improving an Industrial Test Generation Tool using SMT Solver | Hao Ren, Devesh Bhatt and Jan Hvozdovic |
| 2:45-3:00 | The comKorat Tool: Unified Combinatorial and Constraint-based Generation of Structurally Complex Tests | Hua Zhong, Lingming Zhang and Sarfraz Khurshid |
| 3:00-3:15 | Break | |
| 3:15-5:00 | Session: Posters, Tool Demonstrations, and Reception | Location: University Hall |
| Demos: | ||
| ARSENAL: Automatic Requirements Specification Extraction from Natural Language | Natarajan Shankar | |
| Design Contract Export Tool for AGREE | Jing (Janet) Liu | |
| Verifying Relative Safety, Accuracy, and Termination for Program Approximations (+ poster) | Shaobo He | |
| Formal Validation and Verification Framework for Model-Based and Adaptive Control Systems | Michael Yau | |
| Specification and Proof of High-Level Functional Properties of Bit-Level Programs (+ poster) | Claude Marche | |
| The comKorat Tool: Unified Combinatorial and Constraint-based Generation of Structurally Complex Tests | Hua Zhong | |
| Hybrid Systems Model Transformations with HyST | Taylor Johnson | |
| Posters: | ||
| Hierarchical Verification of Quantum Circuits | Sidi Mohamed Beillahi | |
| Temporal Logic Framework for Performance Analysis of Architectures of Systems | Ariane Piel | |
| A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control | Robert Goldman | |
| Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems | Wenchao Li | |
| ConcBugAssist: Constraint Solving for Diagnosis and Repair of Concurrency Bugs | Chao Wang | |
| Quantitative Masking Strength: Quantifying the Power Side-Channel Resistance of Software Code | Chao Wang | |
| Wed, June 8 | ||
| 8:00-8:15 | Check-in/Registration | |
| 8:15-9:15 | Session: Keynote | |
| Where Formal Methods Might Find Application on Future NASA Missions | Michael L. Aguilar | |
| 9:15-9:45 | Break | |
| 9:45-11:30 | Session: Code Generation and Synthesis | Chair: Andrew Gacek |
| 9:45-10:15 | Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty | Susmit Jha and Vasumathi Raman |
| 10:15-10:45 | Obfuscator Synthesis for Privacy and Utility | Yi-Chin Wu, Vasumathi Raman, Stephane Lafortune and Sanjit A. Seshia |
| 10:45-11:15 | Code Generation Using A Formal Model of Reference Counting | Gaspard Ferey and Natarajan Shankar |
| 11:15-11:30 | EventB2Java: A Code Generator for Event-B | Néstor Cataño and Victor Rivera |
| 11:30-1:00 | Lunch | |
| 1:00-3:15 | Session: Applications of Formal Methods | Chair: Kristin Yvonne Rozier |
| 1:00-1:30 | A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles | Albert Rizaldi, Fabian Immler and Matthias Althoff |
| 1:30-2:00 | Probabilistic Formal Verification of the SATS Concept of Operation | Muhammad Usama Sardar, Nida Afaq, Khaza Anuarul Hoque, Taylor T. Johnson and Osman Hasan |
| 2:00-2:15 | Break | |
| 2:15-2:45 | Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application | Josh Newell, Linna Pang, David Tremaine, Alan Wassyng and Mark Lawford |
| 2:45-3:00 | Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft | Cesar Munoz and Anthony Narkawicz |
| 3:00-3:15 | Formal Validation and Verification Framework and Models for Model-Based and Adaptive Control Systems | Sergio Guarro, Umit Ozguner, Tunc Aldemir, Matt Knudson, Arda Kurt, Michael Yau, Mohammad Hejase and Steve Kwon |
| 3:15-3:30 | Break | |
| 3:30-5:00 | Session: Breakouts | Chair: Michael Lowry |
| Connecting the dots between Formal Methods and future NASA Missions | ||
| Thu, June 9 | ||
| 8:00-8:15 | Check-in/Registration | |
| 8:15-9:15 | Keynote | |
| Murphy Was Here | Kevin Driscoll | |
| 9:15-9:45 | Session: Report-back from Breakouts | |
| Connecting the dots between Formal Methods and future NASA Missions | Led by Michael Lowry | |
| 9:45-10:00 | Break | |
| 10:00-11:30 | Session: Techniques for Automated Verification | Chair: Temesghen Kahsai |
| 10:00-10:30 | Verifying Relative Safety, Accuracy, and Termination for Program Approximations | Shaobo He, Shuvendu Lahiri and Zvonimir Rakamaric |
| 10:30-11:00 | Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis | Jeroen Meijer and Jaco van de Pol |
| 11:00-11:30 | Gray-box Learning of Serial Compositions of Mealy Machines | Andreas Abel and Jan Reineke |
| 11:30 -1:00 | Lunch | |
| 1:00-3:15 | Session: Theorem Proving and Proofs | Chair: César Muñoz |
| 1:00-1:30 | Specification and Proof of High-Level Functional Properties of Bit-Level Programs | Clément Fumex, Claire Dross, Jens Gerlach and Claude Marché |
| 1:30-2:00 | Formal Verification of an Executable LTL Model Checker with Partial Order Reduction | Julian Brunner and Peter Lammich |
| 2:00-2:15 | Break | |
| 2:15-2:45 | A Modular Way to Reason About Iteration | Jean-Christophe Filliâtre and Mário Pereira |
| 2:45-3:00 | A Proof Infrastructure for Binary Programs | Ashlie B. Hocking, Benjamin D. Rodes, John C. Knight, Jack W. Davidson and Clark L. Coleman |
| 3:00-3:15 | Hierarchical Verification of Quantum Circuits | Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud and Sofiene Tahar |
| 3:15-3:30 | Break | |
| 3:30-4:45 | Session: Correctness and Certification | Chair: Mike Whalen |
| 3:30-4:00 | Semantics for Locking Specifications | Michael D. Ernst, Damiano Macedonio, Massimo Merro and Fausto Spoto |
| 4:00-4:30 | From Design Contracts to Component Requirements Verification | Jing Janet Liu, John D. Backes, Darren Cofer and Andrew Gacek |
| 4:30-4:45 | A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control | Robert P. Goldman, Daniel Bryce, Michael Pelican, David Musliner and Kyungmin Bae |
| 4:45-5:00 | Closing Remarks |