|
| 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
(SHORT PAPER)
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) |
|
|
NFM 2012 • PROGRAM
