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 updated on Tue May 21 02:21:12 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page