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, Giuseppe Cadavero and Giuseppe Scaglione.
Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks