Proceedings of the First NASA Formal Methods Symposium
In: Automated Verification of Design Patterns with LePUS3; Machine-Checkable Timed CSP; A Game-Theoretic Approach to Branching Time Abstract-Check-Refine Process; Component-Oriented Behavior Extraction for Autonomic System Design; Software Model Checking Without Source Code; Applying Formal Methods to NASA Projects: Transition from Research to Practice; Comparing Techniques for Certified Static Analysis; Theorem Proving in Intel Hardware Design; Formal Methods for Automated Diagnosis of Autosub 6000; A Module Language for Typing by Contracts; Towards Co-Engineering Communicating Autonomous Cyber-Physical Systems; TLA+: Whence, Wherefore, and Whither; Formal Methods Applications in Air Transportation; Generalized Abstract Symbolic Summaries; Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering; Modeling Guidelines for Code Generation in the Railway Signaling Context; Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder; A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing; Introduction of Virtualization Technology to Multi-Process Model Checking; Tactical Synthesis Of Efficient Global Search Algorithms; jFuzz: A Concolic Whitebox Fuzzer for Java; Coloured Petri Net Refinement Specification and Correctness Proof with Coq; Model Checking - My 27-Year Quest to Overcome the State Explosion Problem; From Goal-Oriented Requirements to Event-B Specifications; Stochastic Formal Correctness of Numerical Algorithms; Deductive Verification of Cryptographic Software; (2009-04-01)
Online
report
Topics covered include: Model Checking - My 27-Year Quest to Overcome the State Explosion Problem; Applying Formal Methods to NASA Projects: Transition from Research to Practice; TLA+: Whence, Wherefore, and Whither; Formal Methods Applications in Air Transportation; Theorem Proving in Intel Hardware Design; Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering; Model Checking for Autonomic Systems Specified with ASSL; A Game-Theoretic Approach to Branching Time Abstract-Check-Refine Process; Software Model Checking Without Source Code; Generalized Abstract Symbolic Summaries; A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing; Component-Oriented Behavior Extraction for Autonomic System Design; Automated Verification of Design Patterns with LePUS3; A Module Language for Typing by Contracts; From Goal-Oriented Requirements to Event-B Specifications; Introduction of Virtualization Technology to Multi-Process Model Checking; Comparing Techniques for Certified Static Analysis; Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder; jFuzz: A Concolic Whitebox Fuzzer for Java; Machine-Checkable Timed CSP; Stochastic Formal Correctness of Numerical Algorithms; Deductive Verification of Cryptographic Software; Coloured Petri Net Refinement Specification and Correctness Proof with Coq; Modeling Guidelines for Code Generation in the Railway Signaling Context; Tactical Synthesis Of Efficient Global Search Algorithms; Towards Co-Engineering Communicating Autonomous Cyber-Physical Systems; and Formal Methods for Automated Diagnosis of Autosub 6000.
| Titel: |
Proceedings of the First NASA Formal Methods Symposium
|
|---|---|
| Autor/in / Beteiligte Person: | Denney, Ewen ; Giannakopoulou, Dimitra ; Pasareanu, Corina S |
| Link: | |
| Quelle: | Automated Verification of Design Patterns with LePUS3; Machine-Checkable Timed CSP; A Game-Theoretic Approach to Branching Time Abstract-Check-Refine Process; Component-Oriented Behavior Extraction for Autonomic System Design; Software Model Checking Without Source Code; Applying Formal Methods to NASA Projects: Transition from Research to Practice; Comparing Techniques for Certified Static Analysis; Theorem Proving in Intel Hardware Design; Formal Methods for Automated Diagnosis of Autosub 6000; A Module Language for Typing by Contracts; Towards Co-Engineering Communicating Autonomous Cyber-Physical Systems; TLA+: Whence, Wherefore, and Whither; Formal Methods Applications in Air Transportation; Generalized Abstract Symbolic Summaries; Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering; Modeling Guidelines for Code Generation in the Railway Signaling Context; Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder; A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing; Introduction of Virtualization Technology to Multi-Process Model Checking; Tactical Synthesis Of Efficient Global Search Algorithms; jFuzz: A Concolic Whitebox Fuzzer for Java; Coloured Petri Net Refinement Specification and Correctness Proof with Coq; Model Checking - My 27-Year Quest to Overcome the State Explosion Problem; From Goal-Oriented Requirements to Event-B Specifications; Stochastic Formal Correctness of Numerical Algorithms; Deductive Verification of Cryptographic Software; (2009-04-01) |
| Veröffentlichung: | United States: NASA Center for Aerospace Information (CASI), 2009 |
| Medientyp: | report |
| Schlagwort: |
|
| Sonstiges: |
|