Formal Methods in
Computer-Aided Design
Oct 22 - 25, 2019
Hyatt Place San Jose Downtown, San Jose, California, USA

Accepted Papers

Authors Title Slides Ali Ebnenasir. Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties slides Daniel Neider and Oliver Markgraf. Learning-Based Synthesis of Safety Controllers slides Benjamin Ogles, Peter Aldous and Eric Mercer. Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order slides Alexander Nadel. Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization slides Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs and Matteo Maffei. Verifying Relational Properties using Trace Logic slides Aile Ge-Ernst, Christoph Scholl and Ralf Wimmer. Localizing Quantifiers for DQBF slides Luca Piccolboni, Giuseppe Di Guglielmo and Luca Carloni. KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Designslides Aellison Cassimiro Teixeira Dos Santos, Ben Schneider and Vivek Nigam. TSNsched: Automated Schedule Generation for Time Sensitive Networking slides Daniela Kaufmann, Armin Biere and Manuel Kauers. Verifying Large Multipliers by Combining SAT and Computer Algebra slides Ryan Berryhill and Andreas Veneris. Chasing Minimal Inductive Validity Cores in Hardware Model Checking slides Freark van der Berg and Jaco van de Pol. Concurrent Chaining Hash Map for Software Model Checking Sujit Muduli, Pramod Subramanyan and Sayak Ray. Verification of Authenticated Firmware Loaders slides Roderick Bloem, Hana Chockler, Masoud Ebrahimi and Ofer Strichman. Synthesizing Reactive Systems Using a Robustness Specification slides Florian Frohn and Jürgen Giesl. Proving Non-Termination via Loop Accelerationslides Raj Kumar Gajavelly, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman and Shiladitya Ghosh. Input Elimination Transformations for Scalable Verification and Trace Reconstruction slides Gideon Geier, Philippe Heim, Felix Klein and Bernd Finkbeiner. Synthroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications slides Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, P. Madhusudan and Indranil Gupta. Kaizen: Building a Verified and Performant Blockchain System slides Nina Narodytska, Leonid Ryzhyk, Igor Ganichev and Soner Sevinc. BDD-Based Algorithms for Packet Classification slides Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman and Kristin Yvonne Rozier. Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties slides Meng Wu, Jingbo Wang, Jyotirmoy Deshmukh and Chao Wang. Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems Haniel Barbosa, Andrew Reynolds, Daniel Larraz and Cesare Tinelli. Extending enumerative function synthesis via SMT-driven classification slides Jakub Kuderski, Jorge A. Navas and Arie Gurfinkel. Unification-based Pointer Analysis without Oversharing slides Rafael Dutra, Jonathan Bachrach and Koushik Sen. GuidedSampler: Coverage-guided Sampling of SMT Solutions slides Amer Tahat, Sarang Joshi, Pronnoy Goswami and Binoy Ravindran. Scalable Translation Validation of Unverified Legacy OS Code slides S. Akshay, Jatin Arora, Supratik Chakraborty, Krishna S, Divya Raghunathan and Shetal Shah. Knowledge Compilation for Boolean Functional Synthesis Dmitry Mordvinov and Grigory Fedyukovich. Property Directed Inference of Relational Invariants slides Oliver Kullmann and Ankit Shukla. Autarkies for DQCNF slides