default search action
7. NFM 2015: Pasadena, CA, USA
- Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi:
NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. Lecture Notes in Computer Science 9058, Springer 2015, ISBN 978-3-319-17523-2
Invited Papers
- Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez:
Moving Fast with Software Verification. 3-11 - Viktor Kuncak:
Developing Verified Software Using Leon. 12-15
Regular Papers
- Martín Abadi, Michael Isard:
Timely Rollback: Specification and Verification. 19-34 - Gianluca Amato, Simone Di Nardo Di Maio, Francesca Scozzari:
Sum of Abstract Domains. 35-49 - Étienne André, Giuseppe Lipari, Hoang Gia Nguyen, Youcheng Sun:
Reachability Preservation Based Parameter Synthesis for Timed Automata. 50-65 - Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz:
Compositional Verification of Parameterised Timed Systems. 66-81 - John Backes, Darren D. Cofer, Steven P. Miller, Michael W. Whalen:
Requirements Analysis of a Quad-Redundant Flight Control System. 82-96 - Dragan Bosnacki, Mark Scheffer:
Partial Order Reduction and Symmetry with Multiple Representatives. 97-111 - Alice Dal Corso, Damiano Macedonio, Massimo Merro:
Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks. 112-126 - Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh:
Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems. 127-142 - Aboubakr Achraf El Ghazi, Mana Taghdiri, Mihai Herda:
First-Order Transitive Closure Axiomatization via Iterative Invariant Injections. 143-157 - Andrew N. Fisher, Chris J. Myers, Peng Li:
Reachability Analysis Using Extremal Rates. 158-172 - Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer:
Towards Realizability Checking of Contracts Using Theories. 173-187 - Thomas Gibson-Robinson, Henri Hansen, A. W. Roscoe, Xu Wang:
Practical Partial Order Reduction for CSP. 188-203 - Alex Groce, Jervis Pinto:
A Little Language for Testing. 204-218 - Yu Huang, Eric Mercer:
Detecting MPI Zero Buffer Incompatibility by SMT Encoding. 219-233 - Robert Jakob, Peter Thiemann:
A Falsification View of Success Typing. 234-247 - Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee:
Verified ROS-Based Deployment of Platform-Independent Control Systems. 248-262 - Rajiv Murali, Andrew Ireland, Gudmund Grov:
A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios. 263-278 - Anitha Murugesan, Michael W. Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats Per Erik Heimdahl, Dongjiang You:
Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites. 279-294 - Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen:
A Greedy Approach for the Efficient Repair of Stochastic Models. 295-309 - Yan Peng, Mark R. Greenstreet:
Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification. 310-326 - Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanovic, Philipp Rümmer, Thomas Wies:
Conflict-Directed Graph Coverage. 327-342 - Holger Siegel, Axel Simon:
Shape Analysis with Connectors. 343-358 - Ahlem Triki, Borzoo Bonakdarpour, Jacques Combaz, Saddek Bensalem:
Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models. 359-374 - Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein, Werner Stephan, Burkhart Wolff, Yakoub Nemouchi:
Formal API Specification of the PikeOS Separation Kernel. 375-389
Short Papers
- Ivan Bocic, Tevfik Bultan:
Data Model Bugs. 393-399 - Luis M. Carril, Walter F. Tichy:
Predicting and Witnessing Data Races Using CSP. 400-407 - Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski:
A Benchmark Suite for Hybrid Systems Reachability Analysis. 408-414 - Jesús Aransay, Jose Divasón:
Generalizing a Mathematical Analysis Library in Isabelle/HOL. 415-421 - Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey:
A Tool for Intersecting Context-Free Grammars and Its Applications. 422-428 - Reza Hajisheykhi, Ali Ebnenasir, Sandeep S. Kulkarni:
UFIT: A Tool for Modeling Faults in UPPAAL Timed Automata. 429-435 - Marijn Heule, Martina Seidl, Armin Biere:
Blocked Literals Are Universal. 436-442 - Greg Eakman, Howard Reubenstein, Tom Hawkins, Mitesh Jain, Panagiotis Manolios:
Practical Formal Verification of Domain-Specific Language Applications. 443-449 - Olli Saarikivi, Keijo Heljanko:
Reporting Races in Dynamic Partial Order Reduction. 450-456
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.