3. NFM 2011: Pasadena, CA, USA

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, 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
  
• Simon Foster, Georg Struth:
  Integrating an Automated Theorem Prover into Agda. 116-130
  
• 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
  
• Temesghen Kahsai, Yeting Ge, Cesare Tinelli:
  Instantiation-Based Invariant Discovery. 192-206
  
• Sjoerd Cranen, Jeroen Keiren, Tim A. C. Willemse:
  Stuttering Mostly Speeds Up Solving Parity Games. 207-221
  
• Tsutomu Kumazawa, Tetsuo Tamai:
  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 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
  
• 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 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
  
• 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
  

Last update Fri May 25 08:29:06 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page