Wednesday, 20 October -- Tutorials

8.00 Registration

9.00 - 9:10 Welcome from the USI President

9.10 - 10.30 Tutorial
  Sumit Gulwani
  Dimensions in Program Synthesis
10.30 Coffee Break

11.00 - 12.30 Tutorial
  Kenneth L. McMillan
  Invariant Generation
12.30 Lunch Break

14.15 - 15.45 Tutorial
  Warren Hunt
  Verification of the VIA (Centaur) Nano Microprocessor using the ACL2 Theorem-Proving System
15.45 Coffee Break

16.15 - 17.45 Tutorial
  Jin Yang
  Post Silicon Verification

18.15 Reception at "Il Ciani"
  The historical building located in downton Lugano dates back to the 19th century and is located on a property of about 4.000 square meters enriched by the presence of century old trees. The peculiarity of its pyramid-shaped skylight in glass and metal and the decoration of the round arches and beautiful wooden floor make it a unique venue.

Thursday, 21 October

8.30 Registration

8.45 - 9.00 Welcome
9.00 - 10.00 Invited Talk -- Joseph Sifakis
  Chair: Natasha Sharygina
  Title: Embedded Systems Design Scientific Challenges and Work Directions
10.00 Coffee Break

10.30 -12.15 Industrial Track -- Case Studies
  Chair: Cindy Eisner
10.30 Balekudru Krishna, Anamaya Sullerey and Alok Jain
  Formal Verification of an ASIC Ethernet Switch Block
11.00 Gadiel Auerbach, Fady Copty and Viresh Paruthi
  Formal Verification of Arbiters using Property Strengthening and Underapproximations (short paper)
11.15 Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits and Alexander Nadel
  SAT-Based Semiformal Verification of Hardware
11.45 Lopamudra Sen, Supriya Bhattacharjee, Amit Roy, Bijitendra Mittra and Subir K Roy
  DFT Logic Verification through Property Based Formal Methods -- SOC to IP
12.15 Lunch Break

14.15 - 15.45 Software Verification
  Chair: Aarti Gupta
14.15 Thomas Ball, Ella Bounimova, Rahul Kumar and Vladimir Levin
  SLAM2: Static Driver Verification with Under 4% False Alarms
14.45 Johannes Kinder and Helmut Veith
  Precise Static Analysis of Untrusted Driver Binaries
15.15 Alessandro Cimatti, Andrea Micheli, Iman Narasamdya and Marco Roveri
  Verifying SystemC: a Software Model Checking Approach
15.45 Coffee Break

16.15 - 17.45 Decision Procedures
  Chair: Panagiotis Manolios
16.15 Jason Baumgartner, Michael Case and Hari Mony
  Coping with Moore's Law (and More): Supporting Arrays in State-of-the-Art Model Checkers
16.45 Pierluigi Nuzzo, Alberto Puggelli, Sanjit Seshia and Alberto Sangiovanni-Vincentelli
  CalCS: SMT Solving for Nonlinear Convex Constraints
17.15 Sicun Gao, Malay Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan and Edmund Clarke
  Integrating ICP and LRA Solvers for Deciding Nonlinear Real Arithmetic Problems
17.45 Business meeting

Friday, 22 October

8.30 Registration

9.00 - 10.30 Synthesis
  Chair: Alessandro Cimatti
9.00 ShengYu Shen, Ying Qin, Jianmin Zhang and SiKun Li
  A Halting Algorithm to Determine the Existence of Decoder
9.30 Jad Hamza, Barbara Jobstmann and Viktor Kuncak
  Synthesis for Regular Specifications over Unbounded Domains
10.00 Michael Kuperstein, Martin Vechev and Eran Yahav
  Automatic Inference of Memory Fences
10.30 Coffee Break

11.00 -12.30 Panel
  Chair: Tom Melham
  The Verification Challenge of Low-Level Embedded Software
  Participants: Per Bjesse (Synopsys), Sanjit A. Seshia (UC Berkeley), Jin Yang (Intel), Rafael Zalman (Infineon)
12.30 Lunch Break

14.15 - 15.45 Industrial Track
  Chair: Holger Busch
14.15 Anders Franzen, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani and Jonathan Shalev
  Applying SMT in Symbolic Execution of Microcode
14.45 Ulrich Kuehne, Sven Beyer, Jörg Bormann and John Barstow
  Automated Formal Verification of Processors Based on Architectural Models
15.15 Zurab Khasidashvili, Moshe Emmer, Konstantin Korovin and Andrei Voronkov
  Encoding Industrial Hardware Verification Problems into Effectively Propositional Logic
15.45 Coffee Break

16.15 - 18.00 Hardware and Protocol Verification
  Chair: Jason Baumgartner
16.15 Hamid Savoj, David Berthelot, Alan Mishchenko and Robert Brayton
  Combinational Techniques for Sequential Equivalence Checking (short paper)
16.30 Jun Sawada
  Automatic Verification of Estimate Functions with Polynomials of Bounded Functions
17.00 Peter Boehm
  A Framework for Incremental Modelling and Verification of On-Chip Protocols
17.30 Eyad Alkassar, Ernie Cohen, Mark Hillebrand and Hristo Pentchev
  Modular Specification and Verification of Interprocess Communication
18.30 Social Event | Tour on the Lugano Lake followed by dinner at Capo San Martino.
  The restaurant "Capo San Martino" is located on the promontory facing the Casino of Campione, with a fabulous view on the city of Lugano and the whole bay of the Ceresio lake.

Saturday, 23 October

8.30 Registration

9.00 - 10.00 Invited Talk -- Viresh Paruthi
  Chair: Roderick Bloem
  Title: Large-scale Formal Application: From Fiction to Fact
10.00 Coffee Break

10.30 -12.30 Abstraction
  Chair: Per Bjesse
10.30 Niklas Een, Alan Mishchenko and Nina Amla
  A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction
11.00 Dirk Beyer, M. Erkan Keremoglu and Philipp Wendler
  Predicate Abstraction with Adjustable-Block Encoding
11.30 Nishant Sinha
  Modular Bug Detection with Inertial Refinement
12.00 Joakim Urdahl, Dominik Stoffel, Jörg Bormann, Markus Wedler and Wolfgang Kunz
  Path Predicate Abstraction by Complete Interval Property Checking
12.30 Lunch Break

14.15 - 16.00 SAT and QBF
  Chair: Gianpiero Cabodi
14.15 Leopold Haller and Satnam Singh
  Relieving Capacity Limits on FPGA-based SAT-solvers (short paper)
14.30 Alexander Nadel
  Boosting Minimal Unsatisfiable Core Extraction
15.00 Malay Ganai
  Propelling SAT and SAT-based BMC using Careset
15.30 Christoph Wintersteiger, Youssef Hamadi and Leonardo de Moura
  Efficiently Solving Quantified Bit-Vector Formulas
16.00 Coffee Break

16.30 - 17.45 Verification of Concurrent Systems
  Chair: Armin Biere
16.30 Alfons Laarman, Jaco van de Pol and Michael Weber
  Boosting Multi-Core Reachability Performance with Shared Hash Tables
17.00 Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis and Rongjie Yan
  Incremental Component-based Construction and Verification using Invariants
17.30 Eyad Alkassar, Ernie Cohen, Mark Hillebrand, Mikhail Kovalev and Wolfgang Paul
  Verifying Shadow Page Table Algorithms (short paper)
17.45 Closing