Follow this link to go to the text only version of


NASA - National Aeronautics and Space Administration
Follow this link to skip to the main content
+ Contact NASA
About NASA button News and Events Button Multimedia button Missions button popular topics button MyNASA button
NFM 2012 4th NASA Formal Methods Symposium
NFM 2012 rollover for nfm home page
nfm 2012 rollover for submissions page
nfm 2012 rollover for registration page
NFM 2012 travel rollover
NFM accepted papers rollover
NFM 2012 invited speakers rollover
NFM 2012 Local Information Rollover
NFM 2012 History rollover
  NFM 2012 4th NASA Formal Methods Symposium header image
" "NFM 2012 • PROGRAM


    Tuesday Program weds schedule Thursday Program
  April 5, 2012
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
    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
    Paolo Masci, Huayi Huang, Paul Curzon and Michael Harrison (BibTex)

A Safety Case Pattern for Model-Based Development Approach
    Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky (BibTex)
5:15--5:30 Closing Remarks
    Alwyn Goodloe & Suzette Person



usa gov logo

+ Freedom of Information Act
+ NASA Web Privacy Policy and Important Notices

get adobe reader

get adobe flash player
NASA - National Aeronautics and Space Administration

NASA Official: Suzette Person
Web Curator: Ray Meyer
+ Contact NASA Langley
+ Contact NASA
ast Updated: March 30, 2012