Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2021
Date
2021
Authors
Formal Methods in Computer Aided Design
Journal Title
Journal ISSN
Volume Title
Publisher
TU Wien Academic Press
Abstract
Department
Description
Table of Contents: Tutorials -- Reactive Synthesis Beyond Realizability / by Rayna Dimitrova (p. 1) -- Stainless Verification System Tutorial / by Viktor Kuncak and Jad Hamza (p. 2) -- Formal Methods for the Security Analysis of Smart Contracts / by Matteo Maffei (p. 8) -- Active Automata Learning: from L* to L# / by Frits Vaandrager (p. 9) -- Invited Talks -- From Viewstamped Replication to Blockchains / by Barbara Liskov (p. 10) -- Algorithms for the People / by Seny Kamara (p. 11) -- Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V / by Peter Sewell (p. 12) -- Student Forum -- The FMCAD 2021 Student Forum / by Mark Santolucito (p. 13) -- Hardware -- CocoAlma: A Versatile Masking Verifier / by Vedad Hadžic and Roderick Bloem (p. 14) -- End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers / by Dapeng Gao and Tom Melham (p. 24) -- Hardware Security Leak Detection by Symbolic Simulation / by Neta Bar Kama and Roope Kaivola (p. 34) -- Scaling up Hardware Accelerator Verification using A-QED with Functional Decomposition / by
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 (p. 42) -- Sound and Automated Verification of Real-World RTL Multipliers / by Mertcan Temel and Warren Hunt (p. 53) -- Model Checking and IC3 -- IC3 with Internal Signals / by Rohit Dureja, Arie Gurfinkel, Alexander Ivrii and Yakir Vizel (p. 63) -- Single Clause Assumption without Activation Literals to Speed-up IC3 / by Nils Froleyks and Armin Biere (p. 72) -- Logical Characterization of Coherent Uninterpreted Programs / by Hari Govind Vediramana Krishnan, Sharon Shoham and Arie Gurfinkel (p. 77) -- Data-driven Optimization of Inductive Generalization / by Nham Le, Xujie Si, and Arie Gurfinkel (p. 86) -- Model Checking AUTOSAR Components with CBMC / by Timothee Durand, Katalin Fazekas, Georg Weissenbacher and Jakob Zwirchmayr (p. 96) -- Concurrency and Distributed Systems -- Automating System Configuration / by Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett (p. 102) -- Towards an Automated Proof of Lamport's Paxos / by Aman Goel and Karem A. Sakallah (p. 112) -- Refinement-Based Verification of Device-to-Device Information Flow / by Ning Dong, Roberto Guanciale, and Mads Dam (p. 123) -- Celestial: A Smart Contracts Verification Framework / by Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal (p. 133) -- The Civl Verifier / by Bernhard Kragl and Shaz Qadeer (p. 143) -- Applied Verification and Synthesis -- Synthesizing Pareto-Optimal Interpretations for Black-Box Models / by Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay and Sanjit A. Seshia (p. 153) -- Dynamic Partial Order Reduction for Spinloops / by Michalis Kokologiannakis, Xiaowei Ren and Viktor Vafeiadis (p. 163) -- Robustness Between Weak Memory Models / by Soham Chakraborty (p. 173) -- Pruning and Slicing Neural Networks using Formal Verification / by Ori Lahav and Guy Katz (p. 183) -- Towards Scalable Verification of Deep Reinforcement Learning / by Guy Amir, Michael Schapira, and Guy Katz (p. 193) -- SAT Solving -- Exploiting Isomorphic Subgraphs in SAT / by Alexander Ivrii and Ofer Strichman (p. 204) -- On Decomposition of Maximal Satisfiable Subsets / by Jaroslav Bendı ́k (p. 212) -- Designing Samplers is Easy: The Boon of Testers / by Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel (p. 222) -- SAT-Inspired Eliminations for Superposition / by Petar Vukmirović, Jasmin Blanchette and Marijn Heule (p. 231) -- SAT Solving in the Serverless Cloud / by Alex Ozdemir, Haoze Wu, and Clark Barrett (p. 241) -- SMT and First-Order Logic -- Induction with Recursive Definitions in Superposition / by Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov (p. 246) -- Fair and Adventurous Enumeration of Quantifier Instantiations / by Mikolas Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds (p. 256) -- Mathematical Programming Modulo Strings / by Ankit Kumar and Panagiotis Manolios (p. 261) -- Lookahead in Partitioning SMT / by
Antti Hyvärinen, Matteo Marescotti and Natasha Sharygina (p. 271) -- A Multithreaded Vampire with Shared Persistent Grounding / by Michael Rawson and Giles Reger (p. 280)
LCSH Subject Headings
Citation
Piskac, R., & Whalen, M. W. (Eds.). (2021). Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (Vol. 2). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4