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 schedule weds schedule thurs schedule
  April 3, 2012
7:00 Registration
8:15--8:30 Opening Remarks
    Alwyn Goodloe & Suzette Person
8:30--9:45 Keynote: Andrew Appel
                "Verified Software Toolchain"
9:45--10:00 BREAK
10:00--12:00 Session I: Symbolic Execution and Runtime Verification
Session Chair: Klaus Havelund

Symbolic Execution of Communicating and Hierarchically Composed UML-RT
State Machines

    Karolina Zurowska and Juergen Dingel (BibTex)

Efficient Symbolic Execution of Value-based Data Structures for
Critical Systems

    Jason Belt, Robby, Patrice Chalin, John Hatcliff and Xianghua Deng (BibTex)

CLSE: Closed-Loop Symbolic Execution
    Rupak Majumdar, Indranil Saha, K.C. Shashidhar and Zilong Wang (BibTex)

Runtime Verification with Predictive Semantics
    Xian Zhang, Martin Leucker and Wei Dong (BibTex)
12:00--1:30 LUNCH
1:30--3:30 Session II: Code Generation and Abstraction Refinement
Session Chair: Oksana Tkachuk

Generating Verifiable Java Code from verified PVS specifications

    Leonard Lensink, Sjaak Smetsers and Marko Van Eekelen (BibTex)

On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols

    Michael Backes, Alex Busenius and Catalin Hritcu (BibTex)

Lessons Learnt from the Adoption of Formal Model-based Development
    Alessio Ferrari, Alessandro Fantechi and Stefania Gnesi (BibTex)

Abstract Model Repair
    George Chatzieleftheriou, Borzoo Bonakdarpour, Scott Smolka and
    Panagiotis Katsaros (BibTex)
3:30--3:45 BREAK
3:45--5:45 Session III: Applications of Formal Methods & Short Papers
Session Chair: Ben DiVito

A Case Study in Verification of Embedded Network Software
    Kalyan Regula, Heather Harton, Hampton Smith, Jason Hallstrom,
    Murali Sitaraman and Nigamanth Sridhar (BibTex)

Compositional Verification of Architectural Models
    Darren Cofer, Andrew Gacek, Steven Miller, Michael Whalen, Brian Lavalley
    and Lui Sha (BibTex)

Runtime Verification meets Android Security (SHORT PAPER)
    Andreas Bauer, Jan-Christoph Kuester and Gil Vegliach (BibTex)

Sound formal verification of Linux's USB BP keyboard driver
    Willem Penninckx, Jan Tobias Muehlberg, Jan Smans, Bart Jacobs and
    Frank Piessens (BibTex)

Integrating Statechart Components in Polyglot  (SHORT PAPER)
    Daniel Balasubramanian, Corina Pasareanu, Gabor Karsai, Thomas Pressburger,
    Michael Lowry and Jason Biatek (BibTex)

Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements (SHORT PAPER)
    Wenbin Li, Mirek Truszczynski and Jane Huffman Hayes (BibTex)   



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