Abstract is missing.
- Model Checking - My 27-year Quest to Overcome the State Explosion ProblemEdmund M. Clarke. 1
- Applying Formal Methods to NASA Projects: Transition from Research to PracticeBill Othon. 2
- TLA+: Whence, Wherefore, and WhitherLeslie Lamport. 3
- Formal Methods Applications in Air TransportationTodd Farley. 4
- Theorem Proving in Intel Hardware DesignJohn O'Leary. 5
- Building a Formal Model of a Human-interactive System: Insights into the Integration of Formal Methods and Human Factors EngineeringMatthew L. Bolton, Ellen J. Bass. 6-15
- Model Checking for Autonomic Systems Specified with ASSLEmil Vassev, Mike Hinchey, Aaron J. Quigley. 16-25
- A Game-Theoretic Approach to Branching Time Abstract-Check-Refine ProcessYi Wang, Tetsuo Tamai. 26-35
- Software Model Checking without Source CodeSagar Chaki, James Ivers. 36-45
- Generalized Abstract Symbolic Summaries for Differencing Heap-manipulating ProgramsSuzette Person, Matthew B. Dwyer. 46-55
- A Comparative Study of Randomized Constraint Solvers for Random-Symbolic TestingMitsuo Takaki, Diego Cavalcanti, Rohit Gheyi, Juliano Iyoda, Marcelo d'Amorim, Ricardo Bastos Cavalcante Prudêncio. 56-65
- Component-Oriented Behavior Extraction for Autonomic System DesignTiziana Margaria, Marco Bakera, Christian Wagner, Emil Vassev, Michael G. Hinchey, Bernhard Steffen. 66-75
- Verification of Design Patterns with LePUS3Jonathan Nicholson, Epameinondas Gasparis, Amnon H. Eden, Rick Kazman. 76-85
- A module language for typing by contractsYann Glouche, Jean-Pierre Talpin, Paul Le Guernic, Thierry Gautier. 86-95
- From Goal-Oriented Requirements to Event-B SpecificationsBenjamin Aziz, Alvaro Arenas, Juan Bicarregui, Christophe Ponsard, Philippe Massonet. 96-105
- Introduction of Virtualization Technology to Multi-Process Model CheckingWatcharin Leungwattanakit, Cyrille Valentin Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto. 106-110
- Comparing Techniques for Certified Static AnalysisDavid Cachera, David Pichardie. 111-115
- Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java PathfinderMatt Staats. 116-120
- jFuzz: A Concolic Whitebox Fuzzer for JavaKarthick Jayaraman, David Harvison, Vijay Ganesh, Adam Kiezun. 121-125
- Machine-Checkable Timed CSPThomas Göthel, Sabine Glesner. 126-135
- Stochastic Formal Methods for Hybrid SystemsMarc Daumas, Érik Martin-Dorel, David R. Lester, Annick Truffert. 136-145
- Deductive Verification of Cryptographic SoftwareManuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto, Bárbara Vieira. 146-155
- Coloured Petri net refinement specification, and correctness proof with CoqChristine Choppy, Micaela Mayero, Laure Petrucci. 156-165
- Modeling Guidelines for Code Generation in the Railway Signaling ContextAlessio Ferrari, Alessandro Fantechi, Stefano Bacherini, Niccolò Zingoni. 166-170
- Tactical Synthesis of Efficient Global Search AlgorithmsSrinivas Nedunuri, William R. Cook, Douglas R. Smith. 171-175
- Towards Co-Engineering Communicating Autonomous Cyber-physical SystemsManuela L. Bujorianu, Marius C. Bujorianu. 176-180
- Formal Methods for Automated Diagnosis of Autosub 6000Juhan P. Ernits, Richard Dearden, Miles Pebody. 181-185