Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2019




Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title





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

LCSH Subject Headings