|
| 7:15 |
Registration |
| 8:00--8:15 |
Announcements |
| 8:15--9:30 |
Keynote: Cesare Tinelli
"SMT-based Model Checking" |
| 9:30--10:00 |
BREAK |
| 10:00--12:00 |
Session I: Numerical and Continuous Mathematics
Session Chair: César Muñoz
Rigorous Polynomial Approximations using Taylor Models in Coq
Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero,
Jean-Michel Muller, Ioana Pasca,
Laurence Rideau and Laurent Théry BibTex)
Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study
Aditi Tagore, Diego Zaccai and
Bruce W. Weide (BibTex)
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL
Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre,
Pierre-Loic Garoche, Eric Feron,
Gilberto Perez and Pablo Ascariz (BibTex)
Modifying Test Suite Composition to Enable Effective Predicate-level Statistical Debugging
Ross Gore and Paul Reynolds (BibTex) |
| 12:00--1:30 |
LUNCH |
| 1:30--3:30 |
Session II: Analysis, Verification & Validation
Session Chair: Paul Miner
A semantic analysis of wireless network security protocols
Damiano Macedonio and Massimo
Merro (BibTex)
Specification in PDL with Recursion
Xinxin Liu and Bingtian Xue (BibTex)
Class-Modular Class-Escape Analysis for Object-Oriented Languages
Alexander Herz and Kalmer Apinis (BibTex)
Incremental verification with mode variable invariants in state machines
Temesghen Kahsai, Pierre-Loïc
Garoche, Cesare Tinelli and
Mike Whalen (BibTex) |
| 3:30--3:45 |
BREAK |
| 3:45--5:15 |
Session III: Short Papers
Session Chair: George Hagen
Testing static analyzers with randomly generated programs (SHORT PAPER)
Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr,
Boris Yakobowski and Xuejun Yang (BibTex)
Some Steps into Verification of Exact Real Arithmetic (SHORT PAPER)
Norbert Müller and Christian
Uhrhan (BibTex)
The Use of Rippling to Automate Event-B Invariant Preservation Proofs
(SHORT PAPER)
Yuhui Lin, Alan Bundy and Gudmund Grov (BibTex)
Enhancing the Inverse Method with State Merging (SHORT PAPER)
Étienne André, Laurent Fribourg
and Romain Soulat (BibTex)
Using PVS to investigate incidents through the lens of distributed cognition (SHORT PAPER)
Paolo Masci, Huayi Huang, Paul
Curzon and Michael Harrison (BibTex)
A Safety Case Pattern for Model-Based Development Approach
(SHORT PAPER)
Anaheed Ayoub, Baek-Gyu Kim,
Insup Lee and Oleg Sokolsky (BibTex) |
| 5:15--5:30 |
Closing Remarks
Alwyn Goodloe & Suzette Person |
|
|
NFM 2012 • PROGRAM
