Accepted Papers
We accepted 24 regular and 6 short papers out of 90 submissions.
The proceedings have been published in the IEEE Xplore Digital Library.
Best Paper Award
Eli Arbel, Oleg Rokhlenko and Karen Yorav.
SAT-based Synthesis of Clock Gating Functions using 3-valued Abstraction.
Regular Papers
Leonardo de Moura and Nikolaj Bjorner.
Generalized and Efficient Array Decision Procedures.
Robert Koenighofer, Georg Hofferek and Roderick Bloem.
Debugging Formal Specifications Using Simple Counterstrategies.
Hai Zhou.
Retiming and Resynthesis with Sweep are
Complete for Sequential Transformations.
Sergey Tverdyshev.
A Verified Platform for a Gate-Level Electronic Control Unit.
Dirk Beyer, Alessandro Cimatti, Alberto Griggio,
M. Erkan Keremoglu and Roberto Sebastiani.
Software Model Checking via Large-Block Encoding.
Yakir Vizel and Orna Grumberg.
Interpolation-Sequence Based Model Checking.
Zurab Khasidashvili, Mahmoud Kinanah and Andrei Voronkov.
Verifying Equivalence of Memories Using a First Order Logic Theorem Prover.
Zurab Khasidashvili, Daher Kaiss and Doron Bustan.
A Compositional Theory for Observational Equivalence Checking of Hardware.
Michael Case, Hari Mony, Jason Baumgartner and Robert Kanzelman.
Enhanced Verification by Temporal Decomposition.
Brian Keng and Andreas Veneris.
Scaling VLSI Design Debugging with Interpolation.
William Denman, Behzad Akbarpour, Sofiene Tahar,
Mohamed H. Zaki and Lawrence Paulson.
Automated Formal Verification of Analog Designs using MetiTarski.
Roderick Bloem, Karin Greimel, Thomas Henzinger and Barbara Jobstmann.
Synthesizing Robust Systems.
Angelo Brillout, Daniel Kroening and Thomas Wahl.
Mixed Abstractions for Floating-Point Arithmetic.
Zurab Khasidashvili, Gavriel Gavrielov and Tom Melham.
Assume-Guarantee Validation for STE Properties within an SVA Environment.
Alessandro Cimatti, Jori Dubrovin, Tommi Junttila and Marco Roveri.
Structure-Aware Computation of Predicate Abstraction.
Malay Ganai and Franjo Ivancic.
Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC.
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko,
Jiri Simsa, Satnam Singh and Viktor Vafeiadis.
Finding Heap-Bounds for Hardware Synthesis.
Krishnan Kailas, Viresh Paruthi and Brian Monwai.
Formal Verification of Correctness and Performance of
Random Priority-based Arbiters.
Jason Baumgartner, Hari Mony, Michael Case, Jun Sawada and Karen Yorav.
Scalable Conditional Equivalence Checking:
An Automated Invariant-Generation Based Approach.
Sagar Chaki, Arie Gurfinkel and Ofer Strichman.
Decision Diagrams for Linear Arithmetic.
John O'Leary, Murali Talupur and Mark Tuttle.
Protocol Verification using Flows: An Industrial Experience.
Jyotirmoy Deshmukh and E. Allen Emerson.
Verification of Recursive Methods on Tree-like Data Structures.
Saqib Sohail and Fabio Somenzi.
Safety First: A Two-Stage Algorithm for LTL Games.
Short Papers
He Zhu, Fei He, William N.N. Hung, Xiaoyu Song and Ming Gu.
Data Mining based Decomposition for Assume-Guarantee Reasoning.
Levent Erkok, Magnus Carlsson and Adam Wick.
Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol.
Tom van den Broek and Julien Schmaltz.
Towards a Formally Verified Network-on-Chip.
Sandip Ray and Warren Hunt.
Connecting Pre-silicon and Post-silicon Verification.
Jesse Bingham, Flemming Andersen, John Erickson and Gaurav Singh.
Industrial Strength Refinement Checking.
Subodh Sharma, Ganesh Gopalakrishnan and Eric Mercer.
MCC - A runtime verification tool for MCAPI user applications.