NASA Formal Methods: Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011, Proceedings / Edition 1

by Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, Rajeev Joshi

Overview

This book constitutes the refereed proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, held in Pasadena, CA, USA, in April 2011.
The 26 revised full papers presented together with 12 tool papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 141 submissions. The topics covered by NFM 2011 included but were not limited to: theorem proving, logic model checking, automated testing and simulation, model-based engineering, real-time and shastic systems, SAT and SMT solvers, symbolic execution, abstraction and abstraction refinement, compositional verification techniques; static and dynamic analysis techniques, fault protection, cyber security, specification formalisms, requirements analysis, and applications of formal techniques.

Product Details

ISBN-13:	9783642203978
Publisher:	Springer Berlin Heidelberg
Publication date:	05/27/2011
Series:	Lecture Notes in Computer Science , #6617
Edition description:	2011
Pages:	534
Product dimensions:	6.10(w) x 9.25(h) x 0.05(d)

Table of Contents

I Invited Talks

From Retrospective Verification to Forward-Looking Development K. Rustan M. Leino 1

Specifications for Free Andreas Zeller 2

II Invited Tutorials

The Theory and Practice of SALT Andreas Bauer Martin Leucker 13

VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java Bart Jacobs Jan Smans Pieter Philippaerts Frédéric Vogels Willem Penninckx Prank Piessens 41

Verifying Functional Correctness of C Programs with VCC Michal Moskal 56

III Regular Papers

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution Jason Belt John Hatcliff Robby Patrice Chalin David Hardin Xianghua Deng 58

Approximate Quantifier Elimination for Propositional Boolean Formulae Jörg Brauer Andy King 73

Towards Flight Control Verification Using Automated Theorem Proving William Denman Mohamed H. Zaki Sofiène Tahar Luis Rodrigues 89

Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis Rüdiger Ehlers 101

Integrating an Automated Theorem Prover into Agda Simon Foster Georg Struth 116

Efficient Predicate Abstraction of Program Summaries Arie Gurfinkel Sagar Chaki Samir Sapra 131

Synthesis for PCTL in Parametric Markov Decision Processes Ernst Moritz Hahn Tingling Han Lijun Zhang 146

Formalizing Probabilistic Safety Claims Heber Herencia-Zapana George Hagen Anthony Narkawicz 162

The Open Theory Standard Theory Library Joe Hurd 177

Instantiation-Based Invariant Discovery Temesghen Kahsai Yeting Ge Cesare Tinelli 192

Stuttering Mostly Speeds Up Solving Parity Games Sjoerd Cranen Jeroen J.A. Keiren Tim A.C. Willemse 207

Counterexample-Based Error Localization of Behavior Models Tsutomu Kumazawa Tetsuo Tamai 222

Call Invariants Shuvendu K. Lahiri Shaz Qadeer 237

Symmetry for the Analysis of Dynamic Systems Zarrin Langari Richard Trefler 252

Implementing Cryptographic Primitives in the Symbolic Model Peeter Laud 267

Model Checking Using SMT and Theory of Lists Aleksandar Milicevic Hillel Kugler 282

Automated Test Case Generation with SMT-Solving and Abstract Interpretation Jan Peleska Elena Vorobev Florian Lapschies 298

Generating Data Race Witnesses by an SMT-Based Analysis Mahmoud Said Chao Wang Zijiang Yang Karem Sakallah 313

Applying Atomicity and Model Decomposition to a Space Craft System in Event-B Asieh Salehi Fathabadi Abdolbaghi Rezazadeh Michael Butler 328

A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes Alejandro Sánchez César Sánchez 343

Coral: Solving Complex Constraints for Symbolic PathFinder Matheus Souza Mateus Borges Marcelo d'Amorim Corina S. Pasareanu 359

Automated Formal Verification of the TTEthernet Synchronization Quality Wilfried Steiner Bruno Dutertre 375

Extending the GWV Security Policy and Its Modular Application to a Separation Kernel Sergey Tverdyshev 391

Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties José Vander Meulen Charles Pecheur 406

Towards Informed Swarm Verification Anton Wijs 422

Scaling Up with Event-B: A Case Study Faqing Yang Jean-Pierre Jacquot 438

IV Tool Papers

D-Finder 2: Towards Efficient Correctness of Incremental Design Saddek Bensalem Andreas Griesmayer Axel Legay Thanh-Hung Nguyen Joseph Sifakis Rongjie Yan 453

Infer: An Automatic Program Verifier for Memory Safety of C Programs Cristiano Calcagno Dino Distefano 459

Model Construction and Priority Synthesis for Simple Interaction Systems Chih-Hong Cheng Saddek Bensalem Barbara Jobstmann Rongjie Yan Alois Knoll Harald Ruess 466

OpenJML: JML for Java 7 by Extending OpenJDK David R. Cok 472

jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2 David R. Cok 480

opaal: A Lattice Model Checker Andreas Engelbredt Dalsgaard René Rydhof Hansen Kenneth Yrke Jørgensen Kim Gulstrand Larsen Mads Chr. Olesen Petur Olsen Jirí Srba 487

A Tabular Expression Toolbox for Matlab/Simulink Colin Eles Mark Lawford 494

LLVM2CSP: Extracting CSP Models from Concurrent Programs Moritz Kleine Björn Bartels Thomas Göthel Steffen Helke Dirk Prenzel 500

Multi-Core LTSmin: Marrying Modularity and Scalability Alfons Laarman Jaco van de Pol Michael Weber 506

Ginacra: A C++ Library or Real Algebraic Computations Ulrich Loup Erika Ábrahám 512

Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code Hannes Mehnert 518

Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction José Vander Meulen Charles Pecheur 525

Author Index 533