Formal Methods in
Computer-Aided Design
30 Oct - 2 Nov, 2018
University of Texas, Austin, Texas

Accepted Papers

The following papers have been accepted at FMCAD 2018.

Authors Title Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen and Anthony Fox. A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Rustan Leino, Kasper Luckow, Neha Rungta, Oksana Tkachuk and Carsten Varming. Semantic-based Automated Reasoning for AWS Access Policies using SMT Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadžić, Uwe Egly, Florian Lonsing and Martina Seidl. Expansion-Based QBF Solving Without Recursion Eugene Goldberg. Complete Test Sets And Their Approximations Cristian Mattarei, Makai Mann, Clark Barrett, Ross Daly, Dillon Huff and Pat Hanrahan. CoSA: Integrated Verification for Agile Hardware Design Hernan Ponce-De-Leon, Florian Furbach, Keijo Heljanko and Roland Meyer. BMC with Memory Models as Modules Bjørnar Luteberget, Koen Claessen and Christian Johansen. Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation Sourav Anand and Nadia Polikarpova. Automatic Synchronization for GPU Kernels Thomas Pani, Georg Weissenbacher and Florian Zuleger. Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukas Holik, Ahmed Rezine and Philipp Rummer. Trau: SMT solver for string constraints Peter Backeman, Philipp Ruemmer and Aleksandar Zeljić. Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction Bernhard K. Aichernig, Roderick Bloem, Masoud Ebrahimi, Martin Tappler and Johannes Winter. Automata Learning for Symbolic Execution Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelsk, Mooly Sagiv, and Sharon Shoham. Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems Ivan Gavran and Daniel Neider. Learning Linear Temporal Properties Pavel Cadek, Clemens Danninger, Moritz Sinn and Florian Zuleger. Using Loop Bound Analysis For Invariant Generation Alberto Griggio, Marco Roveri and Stefano Tonetta. Certifying Proofs for LTL Model Checking Alexander Ivrii, Ziv Nevo and Jason Baumgartner. k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms Supratik Chakraborty, Dror Fried, Lucas Martinelli Tabajara and Moshe Vardi. Functional Synthesis via Input-Output Separation Julien Brunel, David Chemouil and Tawa Jeanne. Analyzing the Fundamental Liveness Property of the Chord Protocol Hossein Hojjat and Philipp Ruemmer. The Eldarica Horn Solver Hongce Zhang, Caroline Trippel, Yatin Manerkar, Aarti Gupta, Margaret Martonosi and Sharad Malik. Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification Vikas Rao, Utkarsh Gupta, Irina Ilioaea, Arpitha Srinath, Priyank Kalla and Florian Enescu. Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques Adrian Rebola Pardo and Luís Cruz-Filipe. Complete and Efficient DRAT Proof Checking Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar and Aarti Gupta. Solving Constrained Horn Clauses Using Syntax and Data Viktor Malík, Martin Hruska, Peter Schrammel and Tomas Vojnar. Template-Based Verification of Heap-Manipulating Programs Roberto Cavada, Alessandro Cimatti, Sergio Mover, Mirko Sessa, Arturo Amendola, Giuseppe Cadavero and Giuseppe Scaglione. Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks