


default search action
4. NFM 2012: Norfolk, VA, USA
- Alwyn Goodloe, Suzette Person:

NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Lecture Notes in Computer Science 7226, Springer 2012, ISBN 978-3-642-28890-6 - Cesare Tinelli

:
SMT-Based Model Checking. 1 - Andrew W. Appel:

Verified Software Toolchain. 2 - Patrick Cousot:

Formal Verification by Abstract Interpretation. 3-7 - Dennis Guck, Tingting Han, Joost-Pieter Katoen

, Martin R. Neuhäußer:
Quantitative Timed Analysis of Interactive Markov Chains. 8-23 - Alessio Ferrari

, Alessandro Fantechi, Stefania Gnesi
:
Lessons Learnt from the Adoption of Formal Model-Based Development. 24-38 - Karolina Zurowska, Jürgen Dingel:

Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines. 39-53 - Jörg Brauer, Axel Simon:

Inferring Definite Counterexamples through Under-Approximation. 54-69 - Ross Gore, Paul F. Reynolds Jr.:

Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging. 70-84 - Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller

, Ioana Pasca, Laurence Rideau, Laurent Théry:
Rigorous Polynomial Approximation Using Taylor Models in Coq. 85-99 - Étienne André

, Laurent Fribourg, Romain Soulat:
Enhancing the Inverse Method with State Merging. 100-105 - Alexander Herz, Kalmer Apinis

:
Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages. 106-119 - Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto

, John Regehr, Boris Yakobowski, Xuejun Yang:
Testing Static Analyzers with Randomly Generated Programs. 120-125 - Darren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha:

Compositional Verification of Architectural Models. 126-140 - Anaheed Ayoub, BaekGyu Kim

, Insup Lee, Oleg Sokolsky
:
A Safety Case Pattern for Model-Based Development Approach. 141-146 - Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loïc Garoche, Eric Feron, Gilberto Pérez, Pablo Ascariz:

PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL. 147-161 - Wenbin Li, Jane Huffman Hayes, Miroslaw Truszczynski:

Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements - (Preliminary Results). 162-167 - Norbert Th. Müller, Christian Uhrhan:

Some Steps into Verification of Exact Real Arithmetic. 168-173 - Andreas Bauer, Jan-Christoph Küster, Gil Vegliach:

Runtime Verification Meets Android Security. 174-180 - Xinxin Liu, Bingtian Xue:

Specification in PDL with Recursion. 181-194 - Aditi Tagore, Diego Zaccai, Bruce W. Weide:

Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study. 195-209 - Willem Penninckx, Jan Tobias Mühlberg

, Jan Smans, Bart Jacobs
, Frank Piessens:
Sound Formal Verification of Linux's USB BP Keyboard Driver. 210-215 - Yingke Chen, Hua Mao

, Manfred Jaeger
, Thomas Dyhre Nielsen
, Kim Guldstrand Larsen
, Brian Nielsen
:
Learning Markov Models for Stationary System Behaviors. 216-230 - Yuhui Lin, Alan Bundy, Gudmund Grov:

The Use of Rippling to Automate Event-B Invariant Preservation Proofs. 231-236 - Wenrui Meng, Fei He, Bow-Yaw Wang, Qiang Liu:

Thread-Modular Model Checking with Iterative Refinement. 237-251 - Jiri Barnat, Lubos Brim

, Petr Rockai
:
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. 252-266 - Daniel Balasubramanian, Corina S. Pasareanu, Jason Biatek, Thomas Pressburger, Gabor Karsai

, Michael R. Lowry, Michael W. Whalen:
Integrating Statechart Components in Polyglot. 267-272 - Paolo Masci

, Huayi Huang, Paul Curzon
, Michael D. Harrison
:
Using PVS to Investigate Incidents through the Lens of Distributed Cognition. 273-278 - Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi

, Silvio Ranise
:
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. 279-294 - Jason Belt, Robby, Patrice Chalin, John Hatcliff, Xianghua Deng:

Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. 295-309 - Leonard Lensink

, Sjaak Smetsers, Marko C. J. D. van Eekelen:
Generating Verifiable Java Code from Verified PVS Specifications. 310-325 - David N. Jansen

, Flemming Nielson
, Lijun Zhang:
Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm. 326-340 - George Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka, Panagiotis Katsaros

:
Abstract Model Repair. 341-355 - Rupak Majumdar, Indranil Saha, K. C. Shashidhar, Zilong Wang:

CLSE: Closed-Loop Symbolic Execution. 356-370 - Michael Backes, Alex Busenius, Catalin Hritcu:

On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. 371-387 - Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli

, Mike Whalen:
Incremental Verification with Mode Variable Invariants in State Machines. 388-402 - Damiano Macedonio, Massimo Merro

:
A Semantic Analysis of Wireless Network Security Protocols. 403-417 - Xian Zhang, Martin Leucker

, Wei Dong:
Runtime Verification with Predictive Semantics. 418-432 - Kalyan C. Regula, Hampton Smith, Heather Keown, Jason O. Hallstrom, Nigamanth Sridhar, Murali Sitaraman:

A Case Study in Verification of Embedded Network Software. 433-448 - Peter E. Bulychev, Alexandre David, Kim Guldstrand Larsen

, Axel Legay, Marius Mikucionis
, Danny Bøgsted Poulsen
:
Checking and Distributing Statistical Model Checking. 449-463

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














