Program

Saturday, 28 January


0900 - 1000INVITED TALK
Wolfgang Paul, Saarland University
Cyber War, Formal Verification and Certififed Infrastructure
Chair: Andreas Podelski
  
1000 - 1030Coffee Break 
  
1030 - 1235SESSION 1 : THEORY I 
Chair: Matthew Parkinson
   Paolo Herms, Claude Marché and Benjamin Monate
A Certified Multi-provier Verification Condition Generator
 Sabine Schmaltz and Andrey Shadrin
Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftX
 Gregory Kulczycki, Hampton Smith, Heather Harton, Murali Sitaraman, William Ogden and Joseph Hollingswort
The Location Linking Concept: A Basis for Verification of Code Using Pointers
 Nadia Polikarpova and Michał Moskal
Verifying implementations of security protocols by refinement 
 Thomas Wies, Marco Muniz and Viktor Kuncak
Deciding Functional Lists with Sublist Sets
  
1235 - 1350Lunch Break 
  
1350 - 1450INVITED TUTORIAL
Francesco Logozzo, Microsoft Research
Our Experience with the CodeContracts Static Checker
Chair: Andreas Podelski
  
1450 - 1530Special Session on the VSTTE Software Verification Competition
Chair: Natarajan Shankar
  
1530 - 1600Coffee Break
  
1600 - 1805SESSION 2 : TOOLS 
Chair: Ernie Cohen
 Jean-Christophe Filliatre
Verifying Two Lines of C with Why3: an Exercise in Program Verification
 Milena Vujosevic-Janicic and Viktor Kuncak
Development and Evaluation of LAV: an SMT-Based Error Finding Platform
 Martin Brain and Florian Schanda
A Lightweight Technique for Distributed and Incremental Program Verification
 Loren Segal and Patrice Chalin
A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar
 Florian Merz, Stephan Falke and Carsten Sinz
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR
  
1805 - 1900"5-Minute Madness" Session
  
1930Conference Dinner


Sunday, 29 January


0830 - 0930INVITED TALK
Rupak Majumdar, Max Planck Institute for Software Systems
The Marriage of Exploration and Deduction
Chair: Rajeev Joshi

 
0930 - 1000Coffee Break
  
1000 - 1205SESSION 3 : EXPERIMENTS
Chair: Jean-Christophe Filliatre

Van Tang Nguyen, Daisuke Souma, Goro Hatayama and Hitoshi Ohsaki
Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++
 Hannes Mehnert, Filip Sieczkowski, Lars Birkedal and Peter Sestoft
Formalized Verification of Snapshotable Trees: Separation and Sharing
 Ioannis T. Kassios, Peter Müller and Malte Schwerhoff
Comparing Verification Condition Generation with Symbolic Execution: an Experience Report
 Eyad Alkassar, Ernie Cohen, Mikhail Kovalev and Wolfgang J. Paul
Verification of TLB Virtualization Implemented in C
 Amalinda Post and Jochen Hoenicke
Formalization and Analysis of Real-Time Requirements: a Feasibility Study at BOSCH
  
1205 - 1330Lunch Break
  
1330 - 1430INVITED TUTORIAL
Rustan Leino, Microsoft Research
Developing Verified Programs With Dafny
Chair: Rajeev Joshi
  
1430 - 1500Coffee Break
  
1500 - 1705 SESSION 4 : THEORY II
Chair: Thomas Wies
 Abderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff
Isabelle/Circus : a Process Specification and Verification Environment
 Stephan Falke, Deepak Kapur and Carsten Sinz
Termination Analysis of Imperative Programs Using Bitvector Arithmetic
 Christopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster and Jeffrey S. Foster
Specifying and Verifying the Correctness of Dynamic Software Updates
 Misty Davies, Corina Pasareanu and Vishwanath Raman
Symbolic Execution Enhanced System Testing
 Cristiano Bertolini, Martin Schäf and Pascal Schweitzer
Infeasible Code Detection
  
1705 - 1715Closing Remarks 

Comments