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

Description

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 stochastic 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. Front Matter....Pages - From Retrospective Verification to Forward-Looking Development....Pages 1-1 Specifications for Free....Pages 2-12 The Theory and Practice of SALT....Pages 13-40 VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java....Pages 41-55 Verifying Functional Correctness of C Programs with VCC....Pages 56-57 Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution....Pages 58-72 Approximate Quantifier Elimination for Propositional Boolean Formulae....Pages 73-88 Towards Flight Control Verification Using Automated Theorem Proving....Pages 89-100 Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis....Pages 101-115 Integrating an Automated Theorem Prover into Agda....Pages 116-130 Efficient Predicate Abstraction of Program Summaries....Pages 131-145 Synthesis for PCTL in Parametric Markov Decision Processes....Pages 146-161 Formalizing Probabilistic Safety Claims....Pages 162-176 The OpenTheory Standard Theory Library....Pages 177-191 Instantiation-Based Invariant Discovery....Pages 192-206 Stuttering Mostly Speeds Up Solving Parity Games....Pages 207-221 Counterexample-Based Error Localization of Behavior Models....Pages 222-236 Call Invariants....Pages 237-251 Symmetry for the Analysis of Dynamic Systems....Pages 252-266 Implementing Cryptographic Primitives in the Symbolic Model....Pages 267-281 Model Checking Using SMT and Theory of Lists....Pages 282-297 Automated Test Case Generation with SMT-Solving and Abstract Interpretation....Pages 298-312 Generating Data Race Witnesses by an SMT-Based Analysis....Pages 313-327 Applying Atomicity and Model Decomposition to a Space Craft System in Event-B....Pages 328-342 A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes....Pages 343-358 CORAL: Solving Complex Constraints for Symbolic PathFinder....Pages 359-374 Automated Formal Verification of the TTEthernet Synchronization Quality....Pages 375-390 Extending the GWV Security Policy and Its Modular Application to a Separation Kernel....Pages 391-405 Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties....Pages 406-421 Towards Informed Swarm Verification....Pages 422-437 Scaling Up with Event-B: A Case Study....Pages 438-452 D-Finder 2: Towards Efficient Correctness of Incremental Design....Pages 453-458 Infer: An Automatic Program Verifier for Memory Safety of C Programs....Pages 459-465 Model Construction and Priority Synthesis for Simple Interaction Systems....Pages 466-471 OpenJML: JML for Java 7 by Extending OpenJDK....Pages 472-479 jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2....Pages 480-486 opaal : A Lattice Model Checker....Pages 487-493 A Tabular Expression Toolbox for Matlab/Simulink....Pages 494-499 LLVM2CSP : Extracting CSP Models from Concurrent Programs....Pages 500-505 Multi-Core LTS min : Marrying Modularity and Scalability....Pages 506-511 GiNaCRA : A C++ Library for Real Algebraic Computations....Pages 512-517 Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code....Pages 518-524 Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction....Pages 525-531 Back Matter....Pages -