Formal Methods in
Computer-Aided Design
Yale University

Accepted Papers

FMCAD 2021 Accepted Papers

Authors Title Video Slides
Vedad Hadžić and Roderick Bloem Coco-Alma: A Versatile Masking Verifier Video Slides
Rohit Dureja, Arie Gurfinkel, Alexander Ivrii and Yakir Vizel IC3 with Internal Signals Video Slides
Hari Govind Vediramana Krishnan, Sharon Shoham and Arie Gurfinkel Logical Characterization of Coherent Uninterpreted Programs Video Slides
Dapeng Gao and Tom Melham End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers Video Slides
Neta Bar Kama and Roope Kaivola Hardware Security Leak Detection by Symbolic Simulation Video Slides
Alexander Ivrii and Ofer Strichman Exploiting Isomorphic Subgraphs in SAT Video Slides
Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov Induction with Recursive Definitions in Superposition Video Slides
Nham Le, Xujie Si and Arie Gurfinkel Data-driven Inductive Generalization Video Slides
Ori Lahav and Guy Katz Pruning and Slicing Neural Networks using Formal Verification Video Slides
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett and Subhasish Mitra Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition Video Slides
Timothee Durand, Katalin Fazekas, Georg Weissenbacher and Jakob Zwirchmayr Model Checking AUTOSAR Components with CBMC Video Slides
Jaroslav Bendík On Decomposition of Maximal Satisfiable Subsets Video Slides
Nils Froleyks and Armin Biere Single Clause Assumption without Activation Literals to Speed-up IC3 Video Slides
Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay and Sanjit A. Seshia Synthesizing Pareto-optimal Interpretations for Black-Box Models Video Slides
Michalis Kokologiannakis, Xiaowei Ren and Viktor Vafeiadis Dynamic Partial Order Reductions for Spinloops Video Slides
Bernhard Kragl and Shaz Qadeer The Civl Verifier Video Slides
Mertcan Temel and Warren Hunt Sound and Automated Verification of Real-World RTL Multipliers Video Slides
Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel Designing Samplers is Easy: The Boon of Testers Video Slides
Petar Vukmirović, Jasmin Blanchette and Marijn Heule SAT-Inspired Eliminations for Superposition Video Slides
Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett Automating System Configuration Video Slides
Mikolas Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds Fair and Adventurous Enumeration of Quantifier Instantiations Video Slides
Ankit Kumar and Panagiotis Manolios Mathematical Programming Modulo Strings Video Slides
Aman Goel and Karem A. Sakallah Towards an Automatic Proof of Lamport’s Paxos Video Slides
Antti Hyvärinen, Matteo Marescotti and Natasha Sharygina Lookahead in Partitioning SMT Video Slides
Alex Ozdemir, Haoze Wu and Clark Barrett SAT Solving in the Serverless Cloud Video Slides
Ning Dong, Roberto Guanciale and Mads Dam Refinement-Based Verification of Device-to-Device Information Flow Video Slides
Guy Amir, Michael Schapira and Guy Katz Towards scalable verification of deep reinforcement learning Video Slides
Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal Celestial: A Framework for Verified Smart Contracts Video Slides
Soham Chakraborty Robustness between Weak Memory Models Video Slides
Michael Rawson and Giles Reger A Multithreaded Vampire with Shared Persistent Grounding Video Slides