Formal Methods in
Computer-Aided Design
2-6 October, 2017
TU Wien, Vienna, Austria

Accepted Papers

Murphy Berzish, Vijay Ganesh, Yunhui Zheng . Z3str3: A String Solver with Theory-aware Heuristics
Daniela Ritirc, Armin Biere and Manuel Kauers. Column-Wise Verification of Multipliers Using Computer Algebra
Yen-Sheng Ho, Alan Mishchenko and Robert Brayton. Property Directed Reachability with Word-Level Abstraction
Anastasiia Izycheva and Eva Darulova. On Sound Relative Error Bounds for Floating-Point Arithmetic
M. Ammar Ben Khadra, Dominik Stoffel and Wolfgang Kunz. goSAT: Floating-point Satisfiability as Global Optimization
Hans-Peter Deifel, Christian Dietrich, Merlin Göttlinger, Daniel Lohmann, Stefan Milius and Lutz Schröder. Automatic Verification of Application-Tailored OSEK Kernels
Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru and Sebastien Tixeuil. Parameterized Verification of Algorithms for Oblivious Robots on a Ring
Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei and István Majzik. Theta: a Framework for Abstraction Refinement-Based Model Checking
Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Exact Quantitative Model Checking Using Rational Search
Christopher Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul Jackson and Vijay Nagarajan. Verification of a lazy cache coherence protocol against a weak memory model
Kyungmin Bae and Sicun Gao. Modular SMT-Based Analysis of Nonlinear Hybrid Systems
Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris. Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly
Mattias Roux, Sylvain Conchon, Sava Krstic, Rupak Majumdar and Amit Goel. FAR-Cubicle - A new reachability algorithm
Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal and Shaz Qadeer. Lasso detection using Partial State Caching
Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng. Safety Verification of Phaser Programs
Arie Gurfinkel and Alexander Ivrii. K-Induction without Unrolling
Tom van Dijk, Robert Wille and Robert Meolic. Tagged BDDs: Combining reduction rules from different decision diagram types
Matteo Marescotti, Arie Gurfinkel, Antti Hyvärinen and Natasha Sharygina. Designing Parallel PDR
Rohit Dureja and Kristin Yvonne Rozier. FuseIC3: An Algorithm for Checking Large Design Spaces
Elaheh Ghassabani, Michael Whalen and Andrew Gacek. Efficient Generation of All Minimal Inductive Validity Cores
Freek Verbeek and Nike van Vugt-Hage. Estimating Worst-case Latency of on-chip Interconnects with Formal Simulation
William Hallahan, Ennan Zhai and Ruzica Piskac. Automated Analysis and Repair By Example for Firewalls
Lucas Martinelli Tabajara and Moshe Y. Vardi. Factored Boolean Functional Synthesis
Anthony Widjaja Lin, Yu-Fang Chen, Chih-Duo Hong and Philipp Ruemmer. Learning to prove safety over parameterised concurrent systems
Yakir Vizel, Alexander Nadel and Sharad Malik. Solving Linear Arithmetic with SAT-based Model Checking
Klaus Havelund, Doron Peled and Dogan Ulus. First-order Temporal Logic Monitoring with BDDs
Leonardo Alt, Antti Hyvärinen, Sepideh Asadi and Natasha Sharygina. Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions
Grigory Fedyukovich, Samuel Kaufman and Rastislav Bodik. Sampling Invariants from Frequency Distributions
Alessandro Cimatti, Sergio Mover and Mirko Sessa. SMT-based Analysis of Switching Multi-Domain Linear Kirchhoff Networks