NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


NFM 2013 - PROGRAM

Updated 12 June 2013

TUESDAY, MAY 14, 2013
7:00 Registration
8:00 - 8:30 Welcome
8:30 - 9:30 Key Note: Dr. Ken McMillan
The Importance of Generalization in Automated Proof
9:30 - 10:00 BREAK
10:00 - 11:30 Session: Model Checking
Session Chair: Klaus Havelund

Improved State Space Reductions for LTL Model Checking of C & C++ Programs, Petr Rockai, Jiri Barnat and Lubos Brim.

Regular Model Checking Using Solver Technologies and Automata Learning, Daniel Neider and Nils Jansen.

Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFS-FIFO, Alfons Laarman and David Farago.
11:30 - 1:00 LUNCH
1:00 - 2:00 Invited Talk: Dr. Rajeev Joshi
Managing data for Curiosity, Fun and Profit
2:00 - 2:30 BREAK
2:30 - 4:30 Session: Applications of Formal Methods
Session Chair: Perry Alexander

Evaluating Human-human Communication Protocols with Miscommunication Generation and Model Checking, Matthew Bolton and Ellen Bass.

Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing, Rody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak Smetsers and Marko Van Eekelen.

SMT-based analysis of biological computation, Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi and Hillel Kugler.

Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered Systems, Frédéric Boniol, Michaël Lauer, Claire Pagetti and Jérôme Ermont.
4:30 - 5:00 BREAK
5:00 - 6:00 Session: Poster Introduction Blitz Session
Session Chair: Jim Disbrow

- Verification of Floating Point Programs: From Real Numbers to Floating Point Numbers, Alwyn Goodloe, Cesar Munoz, Florent Kirchner and Loic Correnson

- On Designing an ACL2 C Integer Type Safety Checking Tool, Kevin Krause and Jim Alves-Foss

- Hierarchical Safety Cases, Ewen Denney, Ganesh Pai and Iain Whiteside

- PyNuSMV: NuSMV as a Python Library, Simon Busard and Charles Pecheur

- Formal Verification of a Parameterized Data Aggregation Protocol, Sergio Feo-Arenis and Bernd Westphal

- Extracting Hybrid Automata from Control Code, Steven Lyde and Matthew Might

- OnTrack: An Open Tooling Environment For Railway Verification, Phillip James, Matthew Trumble, Helen Treharne, Markus Roggenbach and Steve Schneider

- Using Language Engineering to Lift Languages and Analyses at the Domain Level, Daniel Ratiu, Markus Voleter, Bernhard Schaetz and Bernd Kolb

- jUnitRV - Adding Runtime Verification to jUnit, Normann Decker, Martin Leucker and Daniel Thoma




WEDNESDAY, MAY 15, 2013
8:00 - 9:00 Key Note: Dr. Alex Aiken
Using Learning Techniques in Invariant Inference
9:00 - 9:30 BREAK
9:30 - 11:30 Session: Static Analysis
Session Chair: Bruno Dutertre

Incremental Invariant Generation using Logic-based Automatic Abstract Transformers, Pierre-Loic Garoche, Temesghen Kahsai and Cesare Tinelli.

Numerical Abstract Domain using Support Functions, Yassamine Seladji and Olivier Bouissou.

Widening as Abstract Domain, Bogdan Mihaila, Alexander Sepp and Axel Simon.

LiquidPi: Inferrable Dependent Session Types, Dennis Griffith and Elsa Gunter.
11:30 - 1:00 LUNCH
1:00 - 2:30 Session: Symbolic Execution
Session Chair: Corina Pasareanu


Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution, Timothy K. Zirkel, Stephen F. Siegel and Timothy McClory.

Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding, Wei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li and Zvonimir Rakamaric.

Bounded Lazy Initialization, Jaco Geldenhuys, Nazareno Aguirre, Marcelo Frias and Willem Visser.
2:30 - 3:00 BREAK
3:00 - 5:00 Session: Theorem Proving
Session Chair: Cesar Munoz

Formal Stability Analysis of Optical Resonators, Umair Siddique, Vincent Aravantinos and Sofiene Tahar.

Formal verification of nonlinear inequalities with Taylor interval approximations, Alexey Solovyev and Thomas Hales.

Verifying the Trusted Platform Module [was: Verifying a Privacy CA Remote Attestation Protocol], Brigid Halling and Perry Alexander.

Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory, Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofiene Tahar.
5:00 - 6:00 Poster Session
6:00 - 8:00 CMU Reception




THURSDAY, MAY 16, 2013
8:00 - 9:00 Session: Complex Systems
Session Chair: Eric Mercer

Enclosing Temporal Evolution of Dynamical Systems Using Numerical Methods, Olivier Bouissou, Alexandre Chapoutot and Adel Djoudi.

Inferring Automata with State-local Alphabet Abstractions, Malte Isberner, Falk Howar and Bernhard Steffen.
9:00 - 9:30 BREAK
9:30 - 11:30 Session: Probabilistic and Statistical Analysis
Session Chair: Dimitra Giannakopoulou

A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select, Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp.

Statistical Model Checking of Wireless Mesh Routing Protocols, Peter Höfner and Annabelle McIver.

On-the-fly Confluence Detection for Statistical Model Checking, Arnd Hartmanns and Mark Timmer.

Optimizing Control Strategy using Statistical Model Checking, Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis, Axel Legay and Dehui Du.
11:30 - 1:00 LUNCH
1:00 - 2:00 Key Note: Dr. John Rushby
The Challenge of High-Assurance Software
2:00 - 2:30 BREAK
2:30 - 4:30 Session: Requirements and Specifications
Session Chair: Cesare Tinelli

From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems, Daniela Remenska, Henri Bal, Jeff Templon, Kees Verstoep, Tim Willemse, Philip Homburg and Adrià Casajús.

Automatically Detecting Inconsistencies in Program Specifications, Aditi Tagore and Bruce Weide.

BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software, Brian Larson, Patrice Chalin and John Hatcliff.

Towards Complete Specifications with an Error Calculus, Quang Loc Le, Asankhaya Sharma, Florin Craciun and Wei-Ngan Chin.
4:30 - 5:00 Closing Remarks
First Gov logo
NASA Logo - nasa.gov