default search action
3. NFM 2011: Pasadena, CA, USA
- Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi:
NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. Lecture Notes in Computer Science 6617, Springer 2011, ISBN 978-3-642-20397-8
Invited Talks
- K. Rustan M. Leino:
From Retrospective Verification to Forward-Looking Development. 1 - Andreas Zeller
:
Specifications for Free. 2-12
Invited Tutorials
- Andreas Bauer, Martin Leucker
The Theory and Practice of SALT. 13-40 - Bart Jacobs
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. 41-55 - Michal Moskal:
Verifying Functional Correctness of C Programs with VCC. 56-57
Regular Papers
- Jason Belt, John Hatcliff, Robby, Patrice Chalin, David S. Hardin, Xianghua Deng:
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. 58-72 - Jörg Brauer, Andy King:
Approximate Quantifier Elimination for Propositional Boolean Formulae. 73-88 - William Denman, Mohamed H. Zaki
Towards Flight Control Verification Using Automated Theorem Proving. 89-100 - Rüdiger Ehlers
Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis. 101-115 - Simon Foster
Integrating an Automated Theorem Prover into Agda. 116-130 - Arie Gurfinkel
Efficient Predicate Abstraction of Program Summaries. 131-145 - Ernst Moritz Hahn, Tingting Han, Lijun Zhang:
Synthesis for PCTL in Parametric Markov Decision Processes. 146-161 - Heber Herencia-Zapana, George Hagen, Anthony Narkawicz:
Formalizing Probabilistic Safety Claims. 162-176 - Joe Hurd:
The OpenTheory Standard Theory Library. 177-191 - Temesghen Kahsai, Yeting Ge, Cesare Tinelli
Instantiation-Based Invariant Discovery. 192-206 - Sjoerd Cranen, Jeroen Keiren
Stuttering Mostly Speeds Up Solving Parity Games. 207-221 - Tsutomu Kumazawa
Counterexample-Based Error Localization of Behavior Models. 222-236 - Shuvendu K. Lahiri, Shaz Qadeer:
Call Invariants. 237-251 - Zarrin Langari, Richard J. Trefler:
Symmetry for the Analysis of Dynamic Systems. 252-266 - Peeter Laud
Implementing Cryptographic Primitives in the Symbolic Model. 267-281 - Aleksandar Milicevic, Hillel Kugler
Model Checking Using SMT and Theory of Lists. 282-297 - Jan Peleska, Elena Vorobev, Florian Lapschies:
Automated Test Case Generation with SMT-Solving and Abstract Interpretation. 298-312 - Mahmoud Said, Chao Wang, Zijiang Yang, Karem A. Sakallah:
Generating Data Race Witnesses by an SMT-Based Analysis. 313-327 - Asieh Salehi Fathabadi, Abdolbaghi Rezazadeh, Michael J. Butler
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. 328-342 - Alejandro Sánchez, César Sánchez
A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes. 343-358 - Matheus Souza, Mateus Borges, Marcelo d'Amorim
CORAL: Solving Complex Constraints for Symbolic PathFinder. 359-374 - Wilfried Steiner, Bruno Dutertre:
Automated Formal Verification of the TTEthernet Synchronization Quality. 375-390 - Sergey Tverdyshev:
Extending the GWV Security Policy and Its Modular Application to a Separation Kernel. 391-405 - José Vander Meulen, Charles Pecheur:
Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties. 406-421 - Anton Wijs
Towards Informed Swarm Verification. 422-437 - Faqing Yang, Jean-Pierre Jacquot:
Scaling Up with Event-B: A Case Study. 438-452
Tool Papers
- Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan:
D-Finder 2: Towards Efficient Correctness of Incremental Design. 453-458 - Cristiano Calcagno, Dino Distefano:
Infer: An Automatic Program Verifier for Memory Safety of C Programs. 459-465 - Chih-Hong Cheng, Saddek Bensalem, Barbara Jobstmann, Rongjie Yan, Alois C. Knoll
Model Construction and Priority Synthesis for Simple Interaction Systems. 466-471 - David R. Cok:
OpenJML: JML for Java 7 by Extending OpenJDK. 472-479 - David R. Cok:
jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2. 480-486 - Andreas Engelbredt Dalsgaard, René Rydhof Hansen
opaal: A Lattice Model Checker. 487-493 - Colin Eles, Mark Lawford:
A Tabular Expression Toolbox for Matlab/Simulink. 494-499 - Moritz Kleine, Björn Bartels, Thomas Göthel, Steffen Helke, Dirk Prenzel:
LLVM2CSP: Extracting CSP Models from Concurrent Programs. 500-505 - Alfons Laarman, Jaco van de Pol, Michael Weber:
Multi-Core LTSmin: Marrying Modularity and Scalability. 506-511 - Ulrich Loup, Erika Ábrahám
GiNaCRA: A C++ Library for Real Algebraic Computations. 512-517 - Hannes Mehnert:
Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. 518-524 - José Vander Meulen, Charles Pecheur:
Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction. 525-531
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-12-26 00:35 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: