|
Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuhäußer.
Quantitative Timed Analysis of Interactive Markov Chains
(Talk, BibTex)
Alessio Ferrari, Alessandro Fantechi and Stefania Gnesi.
Lessons Learnt from the Adoption of Formal Model-based Development
(Talk, BibTex)
Karolina Zurowska and Juergen Dingel.
Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines
(Talk, BibTex)
Joerg Brauer and Axel Simon.
Inferring Definite Counterexamples Through Under-Approximation
(Talk, BibTex)
Ross Gore and Paul Reynolds.
Modifying Test Suite Composition to Enable Effective Predicate-level Statistical Debugging
(Talk, BibTex)
Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela
Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau and Laurent
Théry.
Rigorous Polynomial Approximations using Taylor Models in Coq
(Talk, BibTex)
Étienne André, Laurent Fribourg and Romain Soulat.
Enhancing the Inverse Method with State Merging
(Talk, BibTex)
Alexander Herz and Kalmer Apinis.
Class-Modular Class-Escape Analysis for Object-Oriented Languages
(Talk, BibTex)
Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski and Xuejun Yang.
Testing static analyzers with randomly generated programs
(Talk, BibTex)
Darren Cofer, Andrew Gacek, Steven Miller, Michael Whalen, Brian Lavalley and Lui Sha.
Compositional Verification of Architectural Models
(Talk, BibTex)
Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky.
A Safety Case Pattern for Model-Based Development Approach
(Talk, BibTex)
Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loic Garoche, Eric Feron, Gilberto Perez and Pablo Ascariz.
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL
(Talk, BibTex)
Wenbin Li, Mirek Truszczynski and Jane Huffman Hayes.
Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements
(Talk, BibTex)
Norbert Müller and Christian Uhrhan.
Some Steps into Verification of Exact Real Arithmetic
(Talk, BibTex)
Andreas Bauer, Jan-Christoph Kuester and Gil Vegliach.
Runtime Verification meets Android Security (SHORT PAPER)
(Talk, BibTex)
Xinxin Liu and Bingtian Xue.
Specification in PDL with Recursion
(Talk, BibTex)
Aditi Tagore, Diego Zaccai and Bruce W. Weide.
Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study
(Talk, BibTex)
Willem Penninckx, Jan Tobias Muehlberg, Jan Smans, Bart Jacobs and Frank Piessens.
Sound formal verification of Linux's USB BP keyboard driver
(Talk, BibTex)
Yingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen, Kim G. Larsen and Brian Nielsen.
Learning Markov models for stationary system behaviors
(Talk, BibTex)
Yuhui Lin, Alan Bundy and Gudmund Grov.
The Use of Rippling to Automate Event-B Invariant Preservation Proofs
(Talk, BibTex)
Meng Wenrui, Fei He, Bow-Yaw Wang and Qiang Liu.
Thread-Modular Model Checking with Iterative Refinement
(Talk, BibTex)
Jiri Barnat, Lubos Brim and Petr Rockai.
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
(Talk, BibTex)
Daniel Balasubramanian, Corina Pasareanu, Gabor Karsai, Thomas Pressburger, Michael Lowry and Jason Biatek.
Integrating Statechart Components in Polyglot
(Talk, BibTex)
Paolo Masci, Huayi Huang, Paul Curzon and Michael Harrison.
Using PVS to investigate incidents through the lens of distributed cognition
(Talk, BibTex)
Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi and Silvio Ranise.
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
(Talk, BibTex)
Jason Belt, Robby, Patrice Chalin, John Hatcliff and Xianghua Deng.
Efficient Symbolic Execution of Value-based Data Structures for Critical Systems
(Talk, BibTex)
Leonard Lensink, Sjaak Smetsers and Marko Van Eekelen.
Generating Verifiable Java Code from verified PVS specifications
(Talk, BibTex)
David N. Jansen, Flemming Nielson and Lijun Zhang.
Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm
(Talk, BibTex)
George Chatzieleftheriou, Borzoo Bonakdarpour, Scott Smolka and Panagiotis Katsaros.
Abstract Model Repair
(Talk, BibTex)
Rupak Majumdar, Indranil Saha, K.C. Shashidhar and Zilong Wang.
CLSE: Closed-Loop Symbolic Execution
(Talk, BibTex)
Michael Backes, Alex Busenius and Catalin Hritcu.
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
(Talk, BibTex)
Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli and Mike Whalen.
Incremental verification with mode variable invariants in state machines
(Talk, BibTex)
Damiano Macedonio and Massimo Merro.
A semantic analysis of wireless network security protocols
(Talk, BibTex)
Xian Zhang, Martin Leucker and Wei Dong.
Runtime Verification with Predictive Semantics
(Talk, BibTex)
Kalyan Regula, Heather Harton, Hampton Smith, Jason Hallstrom, Murali Sitaraman and Nigamanth Sridhar.
A Case Study in Verification of Embedded Network Software
(Talk, BibTex)
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis and Danny Bøgsted Poulsen.
Checking & Distributing Statistical Model Checking
(Talk, BibTex)
|
|
NFM 2012 • ACCEPTED PAPERS
