Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017




Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title





October 2-6, 2017, in Vienna Austria
Table of Contents: Invited Papers -- How formal analysis and verification add security to blockchain-based systems / by Shin 'Ichiro Matsuo (p. 1) -- Symbolic Security Analysis using the Tamarin Prover / by Cas Cremers (p. 5) -- Coalition, intrigue, ambush, destruction and pride: herding cats can be challenging / by Jade Alglave (p. 6) -- Automated Formal Reasoning About AWS Systems / by Byron Cook (p. 7) -- Formal Methods in Industrial Dependable Systems Design - The TTTech Example / by Wilfried Steiner (p. 8) -- Hardware Model Checking Competition 2017 / by Armin Biere, Tom van Dijk and Keijo Heljanko (p. 9) -- The FMCAD 2017 Graduate Student Forum / by Keijo Heljanko (p. 10) -- Arithmetric -- goSAT: Floating-point Satisfiability as Global Optimization / by M. Ammar Ben Khadra, Dominik Stoffel and Wolfgang Kunz (p. 11) -- On Sound Relative Error Bounds for Floating-Point Arithmetic / by Anastasiia Izycheva and Eva Darulova (p. 15) -- Column-Wise Verification of Multipliers Using Computer Algebra / by Daniela Ritirc, Armin Biere and Manuel Kauers (p. 23) -- Solving -- Efficient Generation of All Minimal Inductive Validity Cores / by Elaheh Ghassabani, Michael Whalen and Andrew Gacek (p. 31) -- Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions / by Leonardo Alt, Antti Hyvarinen, Sepideh Asadi and Natasha Sharygina (p. 39) -- Solving Linear Arithmetic with SAT-based Model Checking / by Yakir Vizel, Alexander Nadel and Sharad Malik (p. 47) -- Z3str3: A String Solver with Theory-aware Heuristics / by Murphy Berzish, Vijay Ganesh and Yunhui Zheng (p. 55) -- Concurrency and Distributed Systems -- Verification of a lazy cache coherence protocol against a weak memory model / by Christopher Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul Jackson and Vijay Nagarajan (p. 60) -- Safety Verification of Phaser Programs / by Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng (p. 68) -- Learning to prove safety over parameterised concurrent systems / by Yu-Fang Chen, Chih-Duo Hong, Anthony Widjaja Lin and Philipp Ruemmer (p. 76) -- Lasso detection using Partial State Caching / by Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal and Shaz Qadeer (p. 84) -- Probabilistic Systems -- Exact Quantitative Probabilistic Model Checking Using Rational Search / by Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan (p. 92) -- Sampling Invariants from Frequency Distributions / by Grigory Fedyukovich, Samuel Kaufman and Rastislav Bodik (p. 100) -- BDDs -- Tagged BDDs: Combining reduction rules from different decision diagram types / by Tom van Dijk, Robert Wille and Robert Meolic (p. 108) -- First-order Temporal Logic Monitoring with BDDs / by Klaus Havelund, Doron Peled and Dogan Ulus (p. 116) -- Factored Boolean Functional Synthesis / by Lucas Martinelli Tabajara and Moshe Y. Vardi (p. 124) -- IC3 -- Property Directed Reachability with Word-Level Abstraction / by Yen-Sheng Ho, Alan Mishchenko and Robert Brayton (p. 132) -- Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly / by Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris (p. 140) -- K-Induction without Unrolling / by Arie Gurfinkel and Alexander Ivrii (p. 148) -- Designing Parallel PDR / by Matteo Marescotti, Arie Gurfinkel, Antti Hyvarinen and Natasha Sharygina (p. 156) -- FuseIC3: An Algorithm for Checking Large Design Spaces / by Rohit Dureja and Kristin Yvonne Rozier (p. 164) -- FAR-Cubicle - A new reachability algorithm for Cubicle / by Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar and Mattias Roux (p. 172) -- Theta: a Framework for Abstraction Refinement-Based Model Checking / by Tamas Toth, Akos Hajdu, Andras Voros, Zoltan Micskei and Istvan Majzik (p. 176) -- Hybrid Systems -- Modular SMT-Based Analysis of Nonlinear Hybrid Systems / by Kyungmin Bae and Sicun Gao (p. 180) -- SMT-based Analysis of Switching Multi-Domain Linear Kirchhoff Networks / by Alessandro Cimatti, Sergio Mover and Mirko Sessa (p. 188) -- Applications -- Automatic Verification of Application-Tailored OSEK Kernels / by Hans-Peter Deifel, Christian Dietrich, Merlin Gottlinger, Daniel Lohmann, Stefan Milius and Lutz Schroder (p. 196) -- Estimating Worst-case Latency of on-chip Interconnects with Formal Simulation / by Freek Verbeek and Nike van Vugt-Hage (p. 204) -- Parameterized Verification of Algorithms for Oblivious Robots on a Ring / by Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru and Sebastien Tixeuil (p. 212) -- Automated Repair By Example for Firewalls / by William Hallahan, Ennan Zhai and Ruzica Piskac (p. 220)

LCSH Subject Headings