|
| 7:15 |
Registration |
| 8:00--8:15 |
Announcements |
| 8:15--9:30 |
Keynote: Patrick Cousot
"Formal Verification by Abstract Interpretation" |
| 9:30--10:00 |
BREAK |
| 10:00--12:00 |
Session I: Model Checking & SMT
Session Chair: Kristin Rozier
Thread-Modular Model Checking with Iterative Refinement
Meng Wenrui, Fei He, Bow-Yaw Wang and Qiang Liu (BibTex)
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
Jiri Barnat, Lubos Brim and Petr
Rockai (BibTex)
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
Roberto Bruttomesso, Alessandro
Carioni, Silvio Ghilardi and
Silvio Ranise (BibTex)
Inferring Definite Counterexamples Through Under-Approximation
Joerg Brauer and Axel Simon (BibTex) |
| 12:00--1:30 |
LUNCH |
| 1:30--3:30 |
Session II: Statistical Analysis
Session Chair: Anthony Narkawitz
Checking & Distributing Statistical Model Checking
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay,
Marius Mikučionis and Danny Bøgsted Poulsen (BibTex)
Quantitative Timed Analysis of Interactive Markov Chains
Dennis Guck, Tingting Han,
Joost-Pieter Katoen and
Martin R. Neuhäußer (BibTex)
Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm
David N. Jansen, Flemming Nielson
and Lijun Zhang (BibTex)
Learning Markov models for stationary system behaviors
Yingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen,
Kim G. Larsen and Brian Nielsen (BibTex)
|
| 3:30--3:45 |
BREAK |
| 3:45--5:15 |
Panel: The application of Formal Methods at NASA
Moderator: Alwyn Goodloe
Mike Lowry (NASA Ames)
Klaus Havelund(NASA/JPL),
Ricky Butler (NASA Langley)
|
| 6:00--8:00 |
Reception
Kincaid's Restaurant 300 Monticello Avenue, Suite 417
(in the MacArthur Center) |
|
|
NFM 2012 • PROGRAM
