| 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 |
| 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.
|
| 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 |