Proceedings of Formal Methods in Computer Aided Design, FMCAD 2018
Access full-text files
Date
2018
Authors
Formal Methods in Computer Aided Design
Journal Title
Journal ISSN
Volume Title
Publisher
IEEE
Abstract
Department
Description
October 30 – November 2, 2018 in Austin, Texas, USA
Table of Contents: INVITED PAPERS -- Formal Verification of Deep Neural Networks / by Nina Narodytska (p. 1) -- Formal Verification of Unsatisfiability Results / by Marijn Heule (p. 2) -- Deductive Verification of Distributed Protocols in First-Order Logic / by Oded Padon (p. 3) -- Formal Verification of Financial Algorithms with Imandra / by Grant Passmore (p. 4) -- Formal Design, Implementation and Verification of Blockchain Languages / by Grigore Rosu (p. 5) -- The FMCAD 2018 Graduate Student Forum / by Dejan Jovanović and Andrew Reynolds (p. 6) -- HARDWARE -- CoSA: Integrated Verification for Agile Hardware Design / by Cristian Mattarei, Makai Mann, Clark Barrett, Ross Daly, Dillon Huff, and Pat Hanrahan (p. 7) -- ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification / by Hongce Zhang, Caroline Trippel, Yatin Manerkar, Aarti Gupta, Margaret Martonosi, and Sharad Malik (p. 12) -- BMC with Memory Models as Modules / by Hernan Ponce-De-Leon, Florian Furbach, Keijo Heljanko, and Roland Meyer (p. 22) -- QUANTIFIERS AND SAT -- Complete Test Sets and Their Approximations / by Eugene Goldberg (p. 31) -- Expansion-Based QBF Solving Without Recursion / by Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadžić, Uwe Egly, Florian Lonsing, and Martina Seidl (p. 40) -- Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction / by Peter Backeman, Philipp Ruemmer, and Aleksandar Zeljić (p. 50) -- LIVENESS -- Analyzing the Fundamental Liveness Property of the Chord Protocol / by Julien Brunel, David Chemouil, and Jeanne Tawa (p. 60) -- k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms / by Alexander Ivrii, Ziv Nevo, and Jason Baumgartner (p. 69) -- Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems / by Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (p. 74) -- CONCURRENCY -- Automatic Synchronization for GPU Kernels / by Sourav Anand and Nadia Polikarpova (p. 85) -- Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / by Thomas Pani, Georg Weissenbacher, and Florian Zuleger (p. 94) -- VERIFICATION -- Template-Based Verification of Heap-Manipulating Programs / by Viktor Malík, Martin Hruska, Peter Schrammel, and Tomas Vojnar (p. 103) -- Using Loop Bound Analysis for Invariant Generation / by Pavel Cadek, Clemens Danninger, Moritz Sinn, and Florian Zuleger (p. 112) -- Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques / by Vikas Rao, Utkarsh Gupta, Irina Ilioaea, Arpitha Srinath, Priyank Kalla, and Florian Enescu (p. 121) -- LEARNING AND SYNTHESIS -- Automata Learning for Symbolic Execution / by Bernhard K. Aichernig, Roderick Bloem, Masoud Ebrahimi, Martin Tappler, and Johannes Winter (p. 130) -- Functional Synthesis via Input-Output Separation / by Supratik Chakraborty, Dror Fried, Lucas Martinelli Tabajara, and Moshe Vardi (p. 139) -- Learning Linear Temporal Properties / by Ivan Gavran and Daniel Neider (p. 148) -- SMT AND CHC -- The Eldarica Horn Solver / by Hossein Hojjat and Philipp Ruemmer (p. 158) -- Trau: SMT Solver for String Constraints / by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukas Holik, Ahmed Rezine, and Philipp Ruemmer (p. 165) -- Solving Constrained Horn Clauses Using Syntax and Data / by Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta (p. 170) -- RAILS -- Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks / by Roberto Cavada, Alessandro Cimatti, Sergio Mover, Mirko Sessa, Giuseppe Cadavero, and Giuseppe Scaglione (p. 179) -- Design-Time Railway Capacity Verification using SAT Modulo Discrete Event Simulation / by Bjørnar Luteberget, Koen Claessen, and Christian Johansen (p. 188) -- CERTIFICATES -- Complete and Efficient DRAT Proof Checking / by Adrian Rebola Pardo and Luís Cruz-Filipe (p. 197) -- Semantic-based Automated Reasoning for AWS Access Policies using SMT / by John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming (p. 206) -- A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 / by Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, and Anthony Fox (p. 215) -- Certifying Proofs for LTL Model Checking / by Alberto Griggio, Marco Roveri, and Stefano Tonetta (p. 225)
Table of Contents: INVITED PAPERS -- Formal Verification of Deep Neural Networks / by Nina Narodytska (p. 1) -- Formal Verification of Unsatisfiability Results / by Marijn Heule (p. 2) -- Deductive Verification of Distributed Protocols in First-Order Logic / by Oded Padon (p. 3) -- Formal Verification of Financial Algorithms with Imandra / by Grant Passmore (p. 4) -- Formal Design, Implementation and Verification of Blockchain Languages / by Grigore Rosu (p. 5) -- The FMCAD 2018 Graduate Student Forum / by Dejan Jovanović and Andrew Reynolds (p. 6) -- HARDWARE -- CoSA: Integrated Verification for Agile Hardware Design / by Cristian Mattarei, Makai Mann, Clark Barrett, Ross Daly, Dillon Huff, and Pat Hanrahan (p. 7) -- ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification / by Hongce Zhang, Caroline Trippel, Yatin Manerkar, Aarti Gupta, Margaret Martonosi, and Sharad Malik (p. 12) -- BMC with Memory Models as Modules / by Hernan Ponce-De-Leon, Florian Furbach, Keijo Heljanko, and Roland Meyer (p. 22) -- QUANTIFIERS AND SAT -- Complete Test Sets and Their Approximations / by Eugene Goldberg (p. 31) -- Expansion-Based QBF Solving Without Recursion / by Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadžić, Uwe Egly, Florian Lonsing, and Martina Seidl (p. 40) -- Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction / by Peter Backeman, Philipp Ruemmer, and Aleksandar Zeljić (p. 50) -- LIVENESS -- Analyzing the Fundamental Liveness Property of the Chord Protocol / by Julien Brunel, David Chemouil, and Jeanne Tawa (p. 60) -- k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms / by Alexander Ivrii, Ziv Nevo, and Jason Baumgartner (p. 69) -- Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems / by Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (p. 74) -- CONCURRENCY -- Automatic Synchronization for GPU Kernels / by Sourav Anand and Nadia Polikarpova (p. 85) -- Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / by Thomas Pani, Georg Weissenbacher, and Florian Zuleger (p. 94) -- VERIFICATION -- Template-Based Verification of Heap-Manipulating Programs / by Viktor Malík, Martin Hruska, Peter Schrammel, and Tomas Vojnar (p. 103) -- Using Loop Bound Analysis for Invariant Generation / by Pavel Cadek, Clemens Danninger, Moritz Sinn, and Florian Zuleger (p. 112) -- Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques / by Vikas Rao, Utkarsh Gupta, Irina Ilioaea, Arpitha Srinath, Priyank Kalla, and Florian Enescu (p. 121) -- LEARNING AND SYNTHESIS -- Automata Learning for Symbolic Execution / by Bernhard K. Aichernig, Roderick Bloem, Masoud Ebrahimi, Martin Tappler, and Johannes Winter (p. 130) -- Functional Synthesis via Input-Output Separation / by Supratik Chakraborty, Dror Fried, Lucas Martinelli Tabajara, and Moshe Vardi (p. 139) -- Learning Linear Temporal Properties / by Ivan Gavran and Daniel Neider (p. 148) -- SMT AND CHC -- The Eldarica Horn Solver / by Hossein Hojjat and Philipp Ruemmer (p. 158) -- Trau: SMT Solver for String Constraints / by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukas Holik, Ahmed Rezine, and Philipp Ruemmer (p. 165) -- Solving Constrained Horn Clauses Using Syntax and Data / by Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta (p. 170) -- RAILS -- Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks / by Roberto Cavada, Alessandro Cimatti, Sergio Mover, Mirko Sessa, Giuseppe Cadavero, and Giuseppe Scaglione (p. 179) -- Design-Time Railway Capacity Verification using SAT Modulo Discrete Event Simulation / by Bjørnar Luteberget, Koen Claessen, and Christian Johansen (p. 188) -- CERTIFICATES -- Complete and Efficient DRAT Proof Checking / by Adrian Rebola Pardo and Luís Cruz-Filipe (p. 197) -- Semantic-based Automated Reasoning for AWS Access Policies using SMT / by John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming (p. 206) -- A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 / by Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, and Anthony Fox (p. 215) -- Certifying Proofs for LTL Model Checking / by Alberto Griggio, Marco Roveri, and Stefano Tonetta (p. 225)