


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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














