4. VSTTE 2012: Philadelphia, PA, USA

• Wolfgang Paul:
  Cyber War, Formal Verification and Certified Infrastructure. 1
  
• Paolo Herms, Claude Marché, Benjamin Monate:
  A Certified Multi-prover Verification Condition Generator. 2-17
  
• Sabine Schmaltz, Andrey Shadrin:
  Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT. 18-33
  
• Gregory Kulczycki, Hampton Smith, Heather K. Harton, Murali Sitaraman, William F. Ogden, Joseph E. Hollingsworth:
  The Location Linking Concept: A Basis for Verification of Code Using Pointers. 34-49
  
• Nadia Polikarpova, Michal Moskal:
  Verifying Implementations of Security Protocols by Refinement. 50-65
  
• Thomas Wies, Marco Muñiz, Viktor Kuncak:
  Deciding Functional Lists with Sublist Sets. 66-81
  
• K. Rustan M. Leino:
  Developing Verified Programs with Dafny. 82
  
• Jean-Christophe Filliâtre:
  Verifying Two Lines of C with Why3: An Exercise in Program Verification. 83-97
  
• Milena Vujosevic-Janicic, Viktor Kuncak:
  Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description. 98-113
  
• Martin Brain, Florian Schanda:
  A Lightweight Technique for Distributed and Incremental Program Verification. 114-129
  
• Loren Segal, Patrice Chalin:
  A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar. 130-145
  
• Florian Merz, Stephan Falke, Carsten Sinz:
  LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. 146-161
  
• Rupak Majumdar:
  The Marriage of Exploration and Deduction. 162
  
• Nguyen Van Tang, Daisuke Souma, Goro Hatayama, Hitoshi Ohsaki:
  Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++. 163-178
  
• Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft:
  Formalized Verification of Snapshotable Trees: Separation and Sharing. 179-195
  
• Ioannis T. Kassios, Peter Müller, Malte Schwerhoff:
  Comparing Verification Condition Generation with Symbolic Execution: An Experience Report. 196-208
  
• Eyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul:
  Verification of TLB Virtualization Implemented in C. 209-224
  
• Amalinda Post, Jochen Hoenicke:
  Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH. 225-240
  
• Francesco Logozzo:
  Our Experience with the CodeContracts Static Checker - (Invited Tutorial). 241-242
  
• Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff:
  Isabelle/Circus: A Process Specification and Verification Environment. 243-260
  
• Stephan Falke, Deepak Kapur, Carsten Sinz:
  Termination Analysis of Imperative Programs Using Bitvector Arithmetic. 261-277
  
• Christopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster, Jeffrey S. Foster:
  Specifying and Verifying the Correctness of Dynamic Software Updates. 278-293
  
• Misty Davies, Corina S. Pasareanu, Vishwanath Raman:
  Symbolic Execution Enhanced System Testing. 294-309
  
• Cristiano Bertolini, Martin Schäf, Pascal Schweitzer:
  Infeasible Code Detection. 310-325
  

Last update Sat May 25 14:51:01 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page