Program for NFM 2011
The Third NASA Formal Methods Symposium
April 18-20, 2011, Pasadena, CA

Monday April 18

Welcome 8:30-8:45

Invited Talk

Chair: Rajeev Joshi
8:45-9:45 Rustan Leino, Microsoft Research, USA
From Retrospective Verification to Forward-Looking Development

Break 9:45-10:15

Session A: SMT

Chair: Bruno Dutertre
10:15-12:20 Instantiation-Based Invariant Discovery
Temesghen Kahsai, Yeting Ge, Cesare Tinelli

Model Checking Using SMT and Theory of Lists
Aleksandar Milicevic, Hillel Kugler

Automated Test Case Generation with SMT-Solving and Abstract Interpretation
Jan Peleska, Elena Vorobev, Florian Lapschies

Generating Data Race Witnesses by an SMT-based Analysis
Mahmoud Said, Chao Wang, Zijiang Yang, Karem Sakallah

A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
Alejandro Sanchez, Cesar Sanchez

Lunch 12:20-13:45

Invited Tutorial

Chair: Rustan Leino
13:45-14:45 Bart Jacobs, Katholieke Universiteit Leuven, Belgium
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java

Break 14:45-15:15

Session B: Program Verification

Chair: Saddek Bensalem
15:15-16:55 Call invariants
Shuvendu Lahiri, Shaz Qadeer

Efficient Predicate Abstraction of Program Summaries
Arie Gurfinkel, Sagar Chaki, Samir Sapra

CORAL: Solving Complex Constraints for Symbolic PathFinder
Matheus Souza, Mateus Borges, Marcelo d’Amorim, Corina Pasareanu

Bakar Kiasan: Flexible Contract Checking for Critical Systems using Symbolic Execution
Jason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin, and Xianghua Deng

Session C: Tool Demos

Chair: Cesar Sanchez
16:55-17:55 Infer: an Automatic Program Verifier for Memory Safety of C Programs
Cristiano Calcagno, Dino Distefano

OpenJML: JML for Java 7 by extending OpenJDK
David Cok

Kopitiam: modular incremental interactive full functional static verification of Java code
Hannes Mehnert

LLVM2CSP : Extracting CSP Models from Concurrent Programs
Moritz Kleine, Bj¨orn Bartels, Thomas Goethel, Steffen Helke, Dirk Prenzel

Tuesday April 19

Invited Talk

Chair: Klaus Havelund
8:45-9:45 Oege de Moor, University of Oxford, Semmle Inc., UK
Do Coding Standards Improve Software Quality?

Break 9:45-10:15

Session D: Applications

Chair: Cordell Green
10:15-12:20 Towards Flight Control Verification using Automated Theorem Proving
William Denman, Mohamed H. Zaki, Sofiene Tahar, and Luis Rodrigues

Automated Formal Verification of the TTEthernet Synchronization Quality
Wilfried Steiner, Bruno Dutertre

Extending the GWV Security Policy and its Modular Application to a Separation Kernel
Sergey Tverdyshev

Applying Atomicity and Model Decomposition to a Space Craft System in Event-B
Asieh Salehi Fathabadi, Abdolbaghi Rezazadeh, Michael Butler

Scaling up with Event-B: A Case Study
Faqing Yang, Jean-Pierre Jacquot

Lunch 12:20-13:45

Invited Tutorial

Chair: Bart Jacobs
13:45-14:45 Michal Moskal, Microsoft Research, USA
Verifying Functional Correctness of C Programs with VCC

Break 14:45-15:15

Session E: Theory

Chair: John Hatcliff
15:15-16:55 Implementing Cryptographic Primitives in the Symbolic Model
Peeter Laud

Formalizing Probabilistic Safety Claims
Heber Herencia-Zapana, George Hagen, Anthony Narkawicz

Symmetry for the Analysis of Dynamic Systems
Zarrin Langari, Richard Trefler

Stuttering Mostly Speeds Up Solving Parity Games
Jeroen Keiren, Sjoerd Cranen, Tim Willemse

Session F: Tool Demos

Chair: Mike Hinchey
16:55-17:55 jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2
David Cok

A Tabular Expression Toolbox for Matlab/Simulink
Colin Eles, Mark Lawford

GiNaCRA: A C++ Library for Real Algebraic Computations
Ulrich Loup, Erika Abraham

Model Construction and Priority Synthesis for Simple Interaction Systems
Chih-Hong Cheng, Barbara Jobstmann, Saddek Bensalem, Rongjie Yan, Alois Knoll, Harald Ruess

Conference Dinner

Wednesday April 20

Invited Talk

Chair: Mihaela Bobaru
8:45-9:45 Andreas Zeller, Saarland University, Germany
Specifications for Free

Break 9:45-10:15

Session G: Logic Model Checking/Synthesis

Chair: Kristin Rozier
10:15-12:20 Counterexample-Based Error Localization of Behavior Models
Tsutomu Kumazawa, Tetsuo Tamai

Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties
Jose Vander Meulen, Charles Pecheur

Towards Informed Swarm Verification
Anton Wijs

Synthesis for PCTL in Parametric Markov Decision Processes
Ernst Moritz Hahn, Tingting Han, Lijun Zhang

Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis
Rudiger Ehlers

Lunch 12:20-13:45

Invited Tutorial

Chair: Marcelo d'Armorim
13:45-14:45 Andreas Bauer, Australian National University, Australia; and Martin Leucker, University of Luebec, Germany
The Theory and Practice of SALT - Structured Assertion Language for Temporal Logic

Break 14:45-15:15

Session H: Theorem Proving, Decision Procedures

Chair: Cesar Munoz
15:15-16:30 Approximate Quantifier Elimination for Propositional Boolean Formulae
Joerg Brauer, and Andy King

Integrating an Automated Theorem Prover into Agda
Simon Foster, Georg Struth

The OpenTheory Standard Theory Library
Joe Hurd

Session I: Tool Demos

Chair: Martin Leucker
16:30-17:30 D-Finder 2: Towards Efficient Correctness of Incremental Design
Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan

opaal: A Lattice Model Checker
Andreas Engelbredt Dalsgaard, Rene Rydhof Hansen, Kenneth Yrke, Jørgensen, Kim G. Larsen, Mads Chr. Olesen, Petur Olsen, Jiri Srba

Multi-Core LTSmin: Marrying Modularity and Scalability
Alfons Laarman, Jaco van de Pol, Michael Weber

Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction
Jose Vander Meulen, Charles Pecheur

Closing Remarks 17:30-17:45