| Description |
1 online resource (xiii, 458 pages) : illustrations |
| Series |
Lecture notes in computer science, 0302-9743 ; 9058 |
|
LNCS sublibrary. SL 2, Programming and software engineering |
|
Lecture notes in computer science ; 9058. 0302-9743
|
|
LNCS sublibrary. SL 2, Programming and software engineering.
|
| Contents |
Intro -- Preface -- Organization -- Contents -- Invited Papers -- Moving Fast with Software Verification -- 1 Introduction -- 2 Facebook's Software Development Model -- 3 Software Verification in the Perpetual Development Era -- 4 Background: the INFER Static Analyser -- 5 Integration with the Development Infrastructure -- 6 Conclusions -- References -- Developing Verified Software Using Leon -- 1 Overview -- References -- Regular Papers -- Timely Rollback: Specification and Verification -- 1 Introduction -- 2 Model of Computation -- 2.1 Basics of Specifications and Implementations |
|
2.2 Basics of Timely Dataflow -- 2.3 High-Level Specification -- 3 An Assumption on External Outputs -- 4 Auxiliary Concepts -- 4.1 Sequences, Frontiers, Filtering, and Reordering -- 4.2 Expressing Dependencies -- 5 Low-Level Specification (with Rollback) -- 6 Refinement Theorem -- 7 Further Refinements -- 7.1 Approximating the Clock and the Could-Result-in Relation -- 7.2 Precomputations -- 7.3 Choosing Frontiers -- 7.4 Implementing the Guard on Notifications -- 8 Conclusion -- References -- Sum of Abstract Domains -- 1 Introduction -- 2 Notations -- 2.1 Linear Algebra |
|
2.2 Abstract Interpretation -- 2.3 Numerical Domains -- 3 Combining Domains by Minkowski Sum -- 3.1 Ordering -- 3.2 Sum of Standard Domains -- 4 Abstract Operators -- 4.1 Union -- 4.2 Linear Transformations -- 4.3 Translations -- 4.4 Non-deterministic Assignment -- 4.5 Refinement by Linear Inequality -- 4.6 Widening and Narrowing -- 5 An Example -- 6 Precision of Abstract Operators -- 6.1 An Approximate Ordering -- 6.2 Abstraction Function -- 6.3 Linear Refinement -- 6.4 Union and Widening -- 6.5 Other Operators -- 6.6 The Domain Int+Parallelotope |
|
6.7 Analysis Kickoff and Non-deterministic Assignments -- 7 Conclusion -- References -- Reachability Preservation Based Parameter Synthesis for Timed Automata -- 1 Introduction -- 2 Preliminaries -- 3 Solving the EF-Emptiness Problem Using Reachability Preservation -- 3.1 Undecidability of the Preservation of Reachability -- 3.2 Parameter Synthesis Preserving the Reachability -- 3.3 EF-Synthesis Using PRP -- 4 Towards Distributed Parameter Synthesis -- 5 Experimental Comparison -- 5.1 Case Studies -- 5.2 Summary of the Experiments and Discussion -- 6 Conclusion -- References |
|
Compositional Verification of Parameterised Timed Systems -- 1 Introduction -- 2 Preliminaries -- 3 PTSs and Their Semantics -- 4 Compositional Verification of PTSs -- 4.1 Component Invariants -- 4.2 History Clocks and Auxiliary Constraints -- 4.3 Interaction Invariants -- 4.4 Parameterised (VR) -- 5 Experiments -- 6 Conclusion and Future Work -- References -- Requirements Analysis of a Quad-Redundant Flight Control System -- 1 Introduction -- 2 Compositional Verification with AGREE -- 3 Requirements Formalization -- 3.1 QFCS Architecture -- 3.2 Flight Control System |
| Summary |
This book constitutes the refereed proceedings of the 7th International Symposium on NASA Formal Methods, NFM 2015, held in Pasadena, CA, USA, in April 2015. The 24 revised regular papers presented together with 9 short papers were carefully reviewed and selected from 108 submissions. The topics include model checking, theorem proving; SAT and SMT solving; symbolic execution; static analysis; runtime verification; systematic testing; program refinement; compositional verification; security and intrusion detection; modeling and specification formalisms; model-based development; model-based testing; requirement engineering; formal approaches to fault tolerance; and applications of formal methods |
| Notes |
International conference proceedings |
|
Includes author index |
|
Online resource; title from PDF title page (SpringerLink, viewed April 16, 2015) |
| Subject |
Formal methods (Computer science) -- Congresses
|
|
Formal methods (Computer science)
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Havelund, Klaus, 1955- editor.
|
|
Holzmann, Gerard J., editor.
|
|
Joshi, Rajeev, editor.
|
| ISBN |
9783319175249 |
|
3319175246 |
|
