The proceedings are available in two volumes: LNCS 9779 and LNCS 9780.
More information: 
Online versions:

July 19, 2016 [Tutorial Day]
9:00am - 12:00pmParosh Abdulla
Small Models in Parameterized Verification
Vitaly Chipounov
The S2E Platform: Design, Implementation, and Applications
12:00pm - 2:00pmLunch
2:00pm - 5:00pmPaulo Tabuada
Synthesizing Robust Cyber-Physical Systems
Martin Vechev and Pavol Bielik
Machine Learning for Programs
6:30pmCAV Reception
July 20, 2016
8:45am - 9:00amWelcome
9:00am - 10:00amKeynote
Session chair: Azadeh Farzan

Gilles Barthe (IMDEA)
Computer-aided Cryptography
10:00am - 10:30am Break
10:30am - 12:00pmProbabilistic Systems
Session chair: Roopsha Samanta

Krishnendu Chatterjee, Hongfei Fu and Amir Kafshdar Goharshady.
Termination Analysis of Probabilistic Programs through Positivstellensatz’s

Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller and James Worrell.
Markov Chains and Unambiguous Büchi Automata

Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti and Justin Hsu.
Synthesizing Probabilistic Invariants via Doob’s Decompositions

Timon Gehr, Sasa Misailovic and Martin Vechev.
PSI: Exact Symbolic Inference for Probabilistic Programs

Van Chan Ngo, Axel Legay and Vania Joloboff.
PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
[Short Talk]
12:00pm - 2:00pmLunch
2:00pm - 3:30pmSynthesis I
Session chair: Armando Solar-Lezama
Chih-Hong Cheng, Yassine Hamsa and Harald Ruess
Structural Synthesis for GXW Specifications

Bernd Finkbeiner and Felix Klein
Bounded Cycle Synthesis

Tobias Klenze, Sam Bayless and Alan J. Hu
Fast, Flexible, and Minimal CTL Synthesis via SMT

Roderick Bloem, Nicolas Braud-Santoni and Swen Jacobs
Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems

Roderick Bloem and Swen Jacobs
[Short Talk]

Rishabh Singh
SyGuS-COMP Results
[Short Talk]
3:30pm - 4:00pm Break
4:00pm - 5:30pmConstraint-Solving I
Session chair: Ruzica Piskac

Maximiliano Cristia and Gianfranco Rossi
A Decision Procedure for Sets, Binary Relations and Partial Functions

Aina Niemetz, Mathias Preiner and Armin Biere
Precise and Complete Propagation-based Local Search for Satisfiability Modulo Theories

Minh-Thai Trinh, Duc-Hiep Chu and Joxan Jaffar
Progressive Reasoning over Recursively-Defined Strings

Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu and Jie-Hong R. Jiang
String Analysis via Automata Manipulation with Logic Circuit Representation

Bishoksan Kafle, John P. Gallagher and Jose F. Morales
RAHFT: A Tool for Verifying Horn Clauses using Abstract Interpretation and Finite Tree Automata
[Short Talk]
July 21, 2016
8:45am - 10:00am Presentation of CAV Award and Keynote Talk by an Award Winner
Session chair: Ahmed Bouajjani
10:00am - 10:30amBreak
10:30am - 12:00pmModel checking I
Session chair: Aws Albarghouthi

Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta and Sergio Mover
Infinite-state Liveness-to-Safety via Implicit Abstraction and Well-founded Relations

Michael Dooley and Fabio Somenzi
Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances

Fei He, Shu Mao and Bow-Yaw Wang
Learning-based Assume-Guarantee Regression Verification

Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu and Sharon Shoham
Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement

Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez and Martin Schäf
JayHorn: A Framework for Verifying Java programs
[Short Talk]
12:00pm - 2:00pm Lunch
2:00pm - 3:30pmProgram Analysis
Session chair: Sharon Shoham

K. Rustan M. Leino and Clément Pit–Claudel
Trigger Selection Strategies to Stabilize Program Verifiers

Quang Loc Le, Sun Jun and Wei-Ngan Chin
Satisfiability Modulo Heap-Based Programs

Peter Müller, Malte Schwerhoff and Alexander J. Summers
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution

Roman Manevich, Boris Dogadov and Noam Rinetzky
From Shape Analysis to Termination Analysis in Linear Time

Dwight Guth, Chris Hathhorn, Manasvi Saxena, and Grigore Rosu
RV-Match: Practical Semantics-Based Program Analysis
[Short Talk]
3:30pm - 4:00pm Break
4:00pm - 5:30pm Timed and Hybrid Systems
Session chair: Rajeev Alur

Bai Xue, Zhikun She and Arvind Easwaran
Under-Approximating Backward Reachable Sets by Polytopes

Parasara Sridhar Duggirala and Mahesh Viswanathan
Parsimonious Simulations Based Verification of Linear Systems

Pavithra Prabhakar and Miriam García Soto
Counterexample Guided Abstraction Refinement for Stability Analysis

Bouyer Patricia, Colange Maximilien and Markey Nicolas
Symbolic Optimal Reachability in Weighted Timed Automata

Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan and Parasara Sridhar Duggirala
Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
5:30pm - 7:00pm CAV Business Meeting
July 22, 2016
9:00am - 10:00amKeynote
Session chair: Clark Barrett

Gerwin Klein (NICTA and University of New South Wales)
Scaling Up - From Trustworthy seL4 to Trustworthy Systems
10:00am - 10:30am Break
10:30am - 12:00pmVerification in Practice
Session chair: Bow-Yaw Wang

Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta and Kristin Yvonne Rozier
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration

Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst and Jonathan Jacky
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers

Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel and Ali Zaidi
End-to-End Verification of ARM Processors with ISA-Formal

FengWei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li
A Practical Verification Framework for Preemptive OS Kernels

Mark Santolucito, Ennan Zhai and Ruzica Piskac
Probabilistic Automated Language Learning for Configuration Files
12:00pm - 2:00pm Lunch
2:00pm - 3:30pm Concurrency
Session chair: Pavol Cerny

Yu-Fang Chen, Song Lei and Zhilin Wu
The Commutativity Problem of the MapReduce Framework: A Transducer-based Approach

Anthony W. Lin and Philipp Ruemmer
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson and Carl Leonardsson
Stateless Model Checking for POWER

Dmitry Chistikov, Rupak Majumdar and Filip Niksic
Hitting Families of Schedules for Asynchronous Programs

Vladimir Herdt, Hoang M. Le, Daniel Große and Rolf Drechsler
ParCoSS: Efficient Parallelized Compiled Symbolic Simulation
3:30pm - 4:00pmBreak
4:00pm - 5:00pm Constraint-Solving II
Session chair: Thomas Wies

Zhoulai Fu and Zhendong Su
XSat: A Fast Floating-Point Satisfiability Solver

Samuel Drews and Aws Albarghouthi.
Effectively Propositional Interpolants

Przemyslaw Daca, Thomas A. Henzinger and Andrey Kupriyanov
Array Folds Logic
5:30pm - 6:30pm Logic Lounge with Moshe Vardi in memoriam Helmut Veith
Venue: University of Toronto Bahen Building - Room 1160 (short name BA1160) 40 St. George Street Toronto, ON, Canada M5S 2E4
7:00pm - 10:00pmCAV Banquet at Art Gallery of Ontario (directions).
Note: The banquet venue will be open for attendees from 6:45pm. Also, the gallery will be open late for visitors.

July 23, 2016
9:00am - 10:00am Keynote
Session chair: Swarat Chaudhuri

Moshe Vardi (Rice University)
Constrained Sampling and Counting
10:00am - 10:30am Break
10:30am - 12:00pmAutomata and Games
Session chair: Fabio Somenzi

Rajeev Alur, Salar Moarref and Ufuk Topcu
Compositional Synthesis of Reactive Controllers for Multi-Agent Systems

Massimo Benerecetti, Daniele Dell’Erba and Fabio Mogavero
Solving Parity Games via Priority Promotion

Ernst Moritz Hahn, Sven Schewe, Andrea Turrini and Lijun Zhang
A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

Salomon Sickert, Javier Esparza, Stefan Jaax and Jan Křetínský
Limit-Deterministic Büchi Automata for Linear Temporal Logic

Ruediger Ehlers and Vasumathi Raman
Slugs: Extensible GR(1) Synthesis
12:00pm - 2:00pmLunch
2:00pm - 3:30pmSynthesis II
Session chair: Roderick Bloem

Hassan Eldib, Meng Wu and Chao Wang
Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits

Alexander Legg, Nina Narodytska and Leonid Ryzhyk
A SAT-Based Counterexample Guided Method for Unbounded Synthesis

Loris D’Antoni, Roopsha Samanta and Rishabh Singh
Qlose: Program Repair with Quantitative Objectives

Dror Fried, Lucas M. Tabajara and Moshe Y. Vardi
BDD-Based Boolean Functional Synthesis

Bernhard Scholz, Herbert Jordan and Pavle Subotic.
Souffle: On Synthesis of Datalog for Program Analyzers
3:30pm - 4:00pmBreak
4:00pm - 5:30pmModel Checking II
Session chair: Constantin Enea

Grigory Fedyukovich, Arie Gurfinkel and Natasha Sharygina
Property Directed Equivalence via Abstract Simulation

Paul Fiterau-Brostean, Ramon Janssen and Frits Vaandrager
Combining Model Checking and Automata Learning to Analyze TCP Implementations

Anton Wijs
BFS-Based Model Checking of Linear-Time Properties With An Application on GPUs

Michele Sevegnani, Muffy Calder and Michele Sevegnani
BigraphER: rewriting and analysis engine for bigraphs

Dirk Beyer and Matthias Dangl
Verification-Aided Debugging: A Convenient Web-Service for Witness Exploration

Adrien Champion, Alain Mebsout, Christoph Sticksel and Cesare Tinelli
The KIND 2 Model-Checker
5:30pm - 5:45pmClosing