FMCAD 2021: FORMAL METHODS IN COMPUTER-AIDED DESIGN 2021

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

Disclaimer | Powered by EasyChair Smart Program