default search action
5. NFM 2013: Moffett Field, CA, USA
- Guillaume Brat, Neha Rungta, Arnaud Venet:
NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. Lecture Notes in Computer Science 7871, Springer 2013, ISBN 978-3-642-38087-7
Session 1: Model Checking
- Petr Rockai
, Jiri Barnat, Lubos Brim
Improved State Space Reductions for LTL Model Checking of C and C++ Programs. 1-15 - Daniel Neider
Regular Model Checking Using Solver Technologies and Automata Learning. 16-31 - Alfons Laarman
Improved on-the-Fly Livelock Detection. 32-47
Session 2: Applications of Formal Methods
- Matthew L. Bolton, Ellen J. Bass
Evaluating Human-Human Communication Protocols with Miscommunication Generation and Model Checking. 48-62 - Rody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak Smetsers, Marko C. J. D. van Eekelen:
Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing. 63-77 - Boyan Yordanov, Christoph M. Wintersteiger
SMT-Based Analysis of Biological Computation. 78-92
Session 3: Complex Systems
- Frédéric Boniol, Michaël Lauer, Claire Pagetti, Jérôme Ermont:
Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered Systems. 93-107 - Olivier Bouissou, Alexandre Chapoutot
Enclosing Temporal Evolution of Dynamical Systems Using Numerical Methods. 108-123 - Malte Isberner
Inferring Automata with State-Local Alphabet Abstractions. 124-138
Session 4: Static Analysis
- Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. 139-154 - Yassamine Seladji, Olivier Bouissou:
Numerical Abstract Domain Using Support Functions. 155-169 - Bogdan Mihaila, Alexander Sepp, Axel Simon:
Widening as Abstract Domain. 170-184 - Dennis Griffith, Elsa L. Gunter:
LiquidPi: Inferrable Dependent Session Types. 185-197
Session 5: Symbolic Execution
- Timothy K. Zirkel, Stephen F. Siegel, Timothy McClory:
Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution. 198-212 - Wei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li, Zvonimir Rakamaric:
Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding. 213-228 - Jaco Geldenhuys, Nazareno Aguirre, Marcelo F. Frias, Willem Visser:
Bounded Lazy Initialization. 229-243
Session 6: Requirements and Specifications
- Daniela Remenska, Jeff Templon
From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems. 244-260 - Aditi Tagore, Bruce W. Weide:
Automatically Detecting Inconsistencies in Program Specifications. 261-275 - Brian R. Larson, Patrice Chalin, John Hatcliff:
BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software. 276-290 - Quang Loc Le, Asankhaya Sharma, Florin Craciun, Wei-Ngan Chin:
Towards Complete Specifications with an Error Calculus. 291-306
Session 7: Probabilistic and Statistical Analysis
- Christel Baier
A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select. 307-321 - Peter Höfner, Annabelle McIver
Statistical Model Checking of Wireless Mesh Routing Protocols. 322-336 - Arnd Hartmanns
On-the-Fly Confluence Detection for Statistical Model Checking. 337-351 - Alexandre David, Dehui Du, Kim Guldstrand Larsen
Optimizing Control Strategy Using Statistical Model Checking. 352-367
Session 8: Theorem Proving
- Umair Siddique
Formal Stability Analysis of Optical Resonators. 368-382 - Alexey Solovyev, Thomas C. Hales:
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations. 383-397 - Brigid Halling, Perry Alexander:
Verifying a Privacy CA Remote Attestation Protocol. 398-412 - Mohamed Yousri Mahmoud
Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory. 413-427
Short Papers
- Sergio Feo-Arenis, Bernd Westphal:
Formal Verification of a Parameterized Data Aggregation Protocol. 428-434 - Phillip James, Matthew Trumble, Helen Treharne
OnTrack: An Open Tooling Environment for Railway Verification. 435-440 - Alwyn Goodloe, César A. Muñoz
Verification of Numerical Programs: From Real Numbers to Floating Point Numbers. 441-446 - Steven Lyde, Matthew Might:
Extracting Hybrid Automata from Control Code. 447-452 - Simon Busard, Charles Pecheur:
PyNuSMV: NuSMV as a Python Library. 453-458 - Normann Decker, Martin Leucker
jUnitRV-Adding Runtime Verification to jUnit. 459-464 - Daniel Ratiu, Markus Voelter, Bernd Kolb, Bernhard Schätz:
Using Language Engineering to Lift Languages and Analyses at the Domain Level. 465-471 - Kevin Krause, Jim Alves-Foss:
On Designing an ACL2-Based C Integer Type Safety Checking Tool. 472-477 - Ewen Denney, Ganesh Pai, Iain Whiteside:
Hierarchical Safety Cases. 478-483
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.
last updated on 2024-11-15 19:20 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: