1. NFM 2009: Moffett Field, California, USA
Ewen Denney, Dimitra Giannakopoulou, Corina S. Pasareanu (Eds.): First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009. 2009 NASA Conference Proceedings
Invited Talks
- Edmund M. Clarke: Model Checking - My 27-year Quest to Overcome the State Explosion Problem. 1
- Bill Othon: Applying Formal Methods to NASA Projects: Transition from Research to Practice. 2
- Leslie Lamport: TLA+: Whence, Wherefore, and Whither. 3
- Todd Farley: Formal Methods Applications in Air Transportation. 4
- John O'Leary: Theorem Proving in Intel Hardware Design. 5
Model Checking: Techniques and Applications
- Matthew L. Bolton, Ellen J. Bass: Building a Formal Model of a Human-interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering. 6-15
- Emil Vassev, Mike Hinchey, Aaron J. Quigley: Model Checking for Autonomic Systems Specified with ASSL. 16-25
- Yi Wang, Tetsuo Tamai: A Game-Theoretic Approach to Branching Time Abstract-Check-Refine Process. 26-35
Symbolic Execution and Testing
- Suzette Person, Matthew B. Dwyer: Generalized Abstract Symbolic Summaries for Differencing Heap-manipulating Programs. 46-55
- Mitsuo Takaki, Diego Cavalcanti, Rohit Gheyi, Juliano Iyoda, Marcelo d'Amorim, Ricardo Bastos Cavalcante Prudêncio: A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing. 56-65
Design and Specification
- Tiziana Margaria, Marco Bakera, Christian Wagner, Emil Vassev, Michael G. Hinchey, Bernhard Steffen: Component-Oriented Behavior Extraction for Autonomic System Design. 66-75
- Jonathan Nicholson, Epameinondas Gasparis, Amnon H. Eden, Rick Kazman: Verification of Design Patterns with LePUS3. 76-85
- Yann Glouche, Jean-Pierre Talpin, Paul Le Guernic, Thierry Gautier: A module language for typing by contracts. 86-95
- Benjamin Aziz, Alvaro Arenas, Juan Bicarregui, Christophe Ponsard, Philippe Massonet: From Goal-Oriented Requirements to Event-B Specifications. 96-105
Analysis: Evaluations and New Developments (Short Papers)
- Watcharin Leungwattanakit, Cyrille Valentin Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto: Introduction of Virtualization Technology to Multi-Process Model Checking. 106-110
- Matt Staats: Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder. 116-120
- Karthick Jayaraman, David Harvison, Vijay Ganesh, Adam Kiezun: jFuzz: A Concolic Whitebox Fuzzer for Java. 121-125
Deductive Verification
- Marc Daumas, Érik Martin-Dorel, David R. Lester, Annick Truffert: Stochastic Formal Methods for Hybrid Systems. 136-145
- Manuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto, Bárbara Vieira: Deductive Verification of Cryptographic Software. 146-155
- Christine Choppy, Micaela Mayero, Laure Petrucci: Coloured Petri net refinement specification, and correctness proof with Coq. 156-165
Modeling and Synthesis (Short Papers)
- Alessio Ferrari, Alessandro Fantechi, Stefano Bacherini, Niccolò Zingoni: Modeling Guidelines for Code Generation in the Railway Signaling Context. 166-170
- Srinivas Nedunuri, William R. Cook, Douglas R. Smith: Tactical Synthesis of Efficient Global Search Algorithms. 171-175
- Manuela L. Bujorianu, Marius C. Bujorianu: Towards Co-Engineering Communicating Autonomous Cyber-physical Systems. 176-180
- Juhan P. Ernits, Richard Dearden, Miles Pebody: Formal Methods for Automated Diagnosis of Autosub 6000. 181-185
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T214307 by the dblp team