3. NFM 2011: Pasadena, CA, USA
Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi (Eds.): NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. Springer 2011 Lecture Notes in Computer Science 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
- Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, Frank Piessens: 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 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, Sofiène Tahar, Luis Rodrigues: 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
- Arie Gurfinkel, Sagar Chaki, Samir Sapra: 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
- Sjoerd Cranen, Jeroen Keiren, Tim A. C. Willemse: Stuttering Mostly Speeds Up Solving Parity Games. 207-221
- Peeter Laud: Implementing Cryptographic Primitives in the Symbolic Model. 267-281
- 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 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, Corina S. Pasareanu: 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
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 Knoll, Harald Ruess: 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, Kenneth Yrke Jørgensen, Kim Guldstrand Larsen, Mads Chr. Olesen, Petur Olsen, Jirí Srba: opaal: A Lattice Model Checker. 487-493
- 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
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team