NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


Regular Papers:

Frédéric Boniol, Michaël Lauer, Claire Pagetti and Jérôme Ermont. Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered Systems

Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp. A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select

Umair Siddique, Vincent Aravantinos and Sofiene Tahar. Formal Stability Analysis of Optical Resonators

Olivier Bouissou, Alexandre Chapoutot and Adel Djoudi. Enclosing Temporal Evolution of Dynamical Systems Using Numerical Methods

Timothy K. Zirkel, Stephen F. Siegel and Timothy McClory. Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution

Wei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li and Zvonimir Rakamaric. Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding

Peter Höfner Annabelle McIver. Statistical Model Checking of Wireless Mesh Routing Protocols

Daniela Remenska, Henri Bal, Jeff Templon, Kees Verstoep, Tim Willemse, Philip Homburg and Adrià Casajús. From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems

Matthew Bolton and Ellen Bass. Evaluating Human-human Communication Protocols with Miscommunication Generation and Model Checking

Alexey Solovyev and Thomas Hales. Formal verification of nonlinear inequalities with Taylor interval approximations

Pierre-Loic Garoche, Temesghen Kahsai and Cesare Tinelli. Incremental Invariant Generation using Logic-based Automatic Abstract Transformers

Petr Rockai, Jiri Barnat and Lubos Brim. Improved State Space Reductions for LTL Model Checking of C & C++ Programs

Arnd Hartmanns and Mark Timmer. On-the-fly Confluence Detection for Statistical Model Checking

Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis, Axel Legay and Dehui Du. Optmizing Control Strategy using Statistical Model Checking

Yassamine Seladji and Olivier Bouissou. Numerical Abstract Domain using Support Functions

Bogdan Mihaila, Alexander Sepp and Axel Simon. Widening as Abstract Domain

Rody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak Smeters and Marko Van Eekelen. Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing

Daniel Neider and Nils Jansen. Regular Model Checking Using Solver Technologies and Automata Learning

Aditi Tagore and Bruce Weide. Automatically Detecting Inconsistencies in Program Specifications

Malte Isberner, Falk Howar and Bernhard Steffen. Inferring Automata with State-local Alphabet Abstractions

Brigid Halling and Perry Alexander. Verifying a Privacy CA Remote Attestation Protocol

Alfons Laarman and David Farago. Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFS-FIFO

Dennis Griffith and Elsa Gunter. LiquidPi: Inferrable Dependent Session Types

Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi and Hillel Kugler. SMT-based analysis of biological computation

Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofienne Tahar. Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory

Brian Larson, Patrice Chalin and John Hatcliff. BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software

Quang Loc Le, Asankhaya Sharma, Florin Craciun and Wei-Ngan Chin. Towards Complete Specifications with an Error Calculus

Jaco Geldenhuys, Nazareno Aguirre, Marcelo Frias and Willem Visser. Bounded Lazy Initialization

Short Papers:

Sergio Feo-Arenis and Bernd Westphal. Formal Verification of a Parameterized Data Aggregation Protocol

Phillip James, Matthew Trumble, Helen Treharne, Markus Roggenbach and Steve Schneider. OnTrack: An Open Tooling Environment For Railway Verification

Alwyn Goodloe, Cesar Munoz, Florent Kirchner and Loic Correnson. Verification of Floating Point Programs:From Real Numbers to Floating Point Numbers

Steven Lyde and Matthew Might. Extracting Hybrid Automata from Control Code

Simon Busard and Charles Pecheur. PyNuSMV: NuSMV as a Python Library

Normann Decker, Martin Leucker and Daniel Thoma. jUnitRV - Adding Runtime Verification to jUnit

Daniel Ratiu, Markus Voleter, Bernhard Schaetz and Bernd Kolb. Using Language Engineering to Lift Languages and Analyses at the Domain Level

Kevin Krause and Jim Alves-Foss. On Designing an ACL2 C Integer Type Safety Checking Tool

Ewen Denney, Ganesh Pai and Iain Whiteside. Hierarchical Safety Cases

First Gov logo
NASA Logo -