FMCAD 2022: FORMAL METHODS IN COMPUTER-AIDED DESIGN

A
Amir, Guy	Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
B
Bajczi, Levente	Axiomatic Analysis of Distributed Systems
Bao, Yuyan	Bounded Model Checking for LLVM
Bar Kama, Neta	Timed Causal Fanin Analysis for Symbolic Circuit Simulation
Barbosa, Haniel	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Barrett, Clark	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers On Optimizing Back-Substitution Methods for Neural Network Verification Neural Network Verification with Proof Production Strategies for Parallel SMT Solving On Optimizing Back-Substitution Methods for Neural Network Verification Proof Production for Neural Network Verification Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Beckett, Ryan	ACORN: Network Control Plane Abstraction using Route Nondeterminism
Bhayat, Ahmed	The Rapid Software Verification Framework
Biere, Armin	Stratified Certification for k-Induction First-Order Subsumption via SAT Solving
Blicha, Martin	Split Transition Power Abstraction for Unbounded Safety
Bloem, Roderick	Reactive Synthesis Modulo Theories using Abstraction Refinement
Bryant, Randal	TBUDDY: A Proof-Generating BDD Package
Bucev, Mario	Formally Verified Quite OK Image Format
C
Chattopadhyay, Saranyu	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
Chen, Fa-Hsun	Reducing NEXP-complete problems to DQBF
Coward, Samuel	Small Proofs from Congruence Closure
D
D'Antoni, Loris	Synthesizing Transducers from Complex Specifications
Daly, Ross	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Dam, Mads	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Dardik, Ian	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
Dobos-Kovács, Mihály	Lazy abstraction for time in eager CEGAR
Dong, Ning	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Donovick, Caleb	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Drechsler, Rolf	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
E
Ebnenasir, Ali	Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables
Ehlers, Rüdiger	Synthesizing Transducers from Complex Specifications
Ene, Cristian	BaxMC: a CEGAR approach to MAX#SAT
Esen, Zafer	TriCera: Verifying C Programs Using the Theory of Heaps
F
Farzan, Azadeh	Commutativity in Concurrent Program Verification
Fedyukovich, Grigory	Split Transition Power Abstraction for Unbounded Safety
Flatt, Oliver	Small Proofs from Congruence Closure
Frolyeks, Nils	Stratified Certification for k-Induction
G
Georgiou, Pamina	The Rapid Software Verification Framework
Gleiss, Bernhard	The Rapid Software Verification Framework
Godbole, Adwait	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results
Greve, David	Enumerative Data Types with Constraints
Grover, Anvay	Synthesizing Transducers from Complex Specifications
Große, Daniel	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Gstrein, Bernhard	Tuning the Learning of Circuit-Based Classifiers
Guanciale, Roberto	Formally Verified Isolation of DMA Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Gupta, Aarti	ACORN: Network Control Plane Abstraction using Route Nondeterminism
Gupta, Aarti	Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
Gurfinkel, Arie	Bounded Model Checking for LLVM
H
Haglund, Jonas	Formally Verified Isolation of DMA
Hanrahan, Pat	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Heljanko, Keijo	Stratified Certification for k-Induction
Heule, Marijn	Compact Symmetry Breaking for Tournaments
Huang, Shen-Chang	Reducing NEXP-complete problems to DQBF
Huvar, Ondřej	Symbolic Coloured Model Checking for HCTL
Hyvärinen, Antti	Split Transition Power Abstraction for Unbounded Safety
I
Isac, Omri	Neural Network Verification with Proof Production Proof Production for Neural Network Verification
J
Jacobs, Swen	Automatic Repair and Deadlock Detection for Parameterized Systems
Jeannin, Jean-Baptiste	Automating Geometric Proofs of Collision Avoidance with Active Corners
Jonsson, Bengt	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
K
Kaivola, Roope	Error Correction Code Algorithm and Implementation Verification using Symbolic Representations Timed Causal Fanin Analysis for Symbolic Circuit Simulation
Kalita, Pankaj Kumar	GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models Synthesis of Semantic Actions in Attribute Grammars
Katz, Guy	On Optimizing Back-Substitution Methods for Neural Network Verification Verification-Aided Deep Ensemble Selection Neural Network Verification with Proof Production Verification-Driven Ensemble Selection On Optimizing Back-Substitution Methods for Neural Network Verification Proof Production for Neural Network Verification
Kheterpal, Nishant	Automating Geometric Proofs of Collision Avoidance with Active Corners
Klumpp, Dominik	Commutativity in Concurrent Program Verification
Konrad, Alexander	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Kovacs, Laura	First-Order Subsumption via SAT Solving The Rapid Software Verification Framework
Kumar, Miriyala Jeevan	Synthesis of Semantic Actions in Attribute Grammars
Kunčak, Viktor	Formally Verified Quite OK Image Format
L
Lachnitt, Hanna	Fine-Grained Reconstruction of cvc5 Proofs in Isabelle/HOL
Lambert, Chris	Compact Symmetry Breaking for Tournaments
Lauffer, Niklas	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Li, Yannan	Proving Robustness of KNNs Against Adversarial Data Poisoning
Liang, Victor	INC: A Scalable Incremental Weighted Sampler
Liang, Victor	Incremental Weighted Sampling
Lohn, Evan	Compact Symmetry Breaking for Tournaments
Lu, Yu-Cheng	Reducing NEXP-complete problems to DQBF
Lång, Magnus	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Lööw, Andreas	Reconciling Verified-Circuit Development and Verilog Development
M
Maderbacher, Benedikt	Reactive Synthesis Modulo Theories using Abstraction Refinement
Mahzoon, Alireza	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Manerkar, Yatin A.	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results
Manolios, Panagiotis	Enumerative Data Types with Constraints
Mehta, Mihir Parang	Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
Melchert, Jack	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Molnár, Vince	Axiomatic Analysis of Distributed Systems Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
Monniaux, David	BaxMC: a CEGAR approach to MAX#SAT
Mounier, Laurent	BaxMC: a CEGAR approach to MAX#SAT
N
Nair, Abhishek	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
Namjoshi, Kedar	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
Niemetz, Aina	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Noetzli, Andres	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
O
Ozdemir, Alex	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
P
Palmskog, Karl	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Panchekha, Pavel	Small Proofs from Congruence Closure
Paxian, Tobias	Trading Accuracy For Smaller Cardinality Constraints
Pereira, Mário	Formal Verification of Algebraic Effects
Podelski, Andreas	Commutativity in Concurrent Program Verification
Potet, Marie-Laure	BaxMC: a CEGAR approach to MAX#SAT
Preiner, Mathias	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Priya, Siddharth	SEAURCHIN: Bounded Model Checking for Rust Bounded Model Checking for LLVM
R
Raghunathan, Divya	ACORN: Network Control Plane Abstraction using Route Nondeterminism
Raina, Priyanka	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Rath, Jakob	First-Order Subsumption via SAT Solving
Rawson, Michael	The Rapid Software Verification Framework
Reger, Giles	The Rapid Software Verification Framework
Reynolds, Andrew	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Roy, Subhajit	GAMBIT: An Interactive Playground for Concurrent Programs Under Relaxed Memory Models Synthesis of Semantic Actions in Attribute Grammars
Ruemmer, Philipp	TriCera: Verifying C Programs Using the Theory of Heaps
S
S. Meel, Kuldeep	INC: A Scalable Incremental Weighted Sampler Incremental Weighted Sampling
Sagonas, Kostis	Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Sahoo, Debashis	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
Sakr, Mouhammad	Automatic Repair and Deadlock Detection for Parameterized Systems
Sallinger, Sarah	A Formalization of Heisenbugs and Their Causes
Sardar, Muhammad Usama	Understanding Trust Assumptions for Attestation in Confidential Computing
Schapira, Michael	Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection
Schlichtkrull, Anders	Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Scholl, Christoph	Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Schou, Morten Konggaard	Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Schultz, William	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
Seshia, Sanjit A.	Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Setaluri, Raj	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Shah, Ameesh	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Sharygina, Natasha	Split Transition Power Abstraction for Unbounded Safety
Singh, Vaibhav	Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
Soares, Tiago	Formal Verification of Algebraic Effects
Srba, Jiri	Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Su, Yusen	Bounded Model Checking for LLVM
Szekeres, Dániel	Lazy Abstraction for Probabilistic Systems
T
Tan, Tony	Reducing NEXP-complete problems to DQBF
Tang, Elanor	Automating Geometric Proofs of Collision Avoidance with Active Corners
Tatlock, Zachary	Small Proofs from Congruence Closure
Telbisz, Csanád	Partial Order Reduction for Abstraction-Based Verification of Concurrent Software
Tinelli, Cesare	Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Traytel, Dmitriy	Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Trefler, Richard	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
Tripakis, Stavros	Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
Tsiskaridze, Nestan	Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
V
Vazquez-Chanlatte, Marcell	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Vigouroux, Thomas	BaxMC: a CEGAR approach to MAX#SAT
Vizel, Yakir	Bounded Model Checking for LLVM
Vo, Daniella	Formal Approach to Identifying Genes and Microbes Significant to Inflammatory Bowel Disease
Völp, Marcus	Automatic Repair and Deadlock Detection for Parameterized Systems
W
Walker, David	ACORN: Network Control Plane Abstraction using Route Nondeterminism
Walter, Andrew T	Enumerative Data Types with Constraints
Wang, Chao	Proving Robustness of KNNs Against Adversarial Data Poisoning
Wang, Jingbo	Proving Robustness of KNNs Against Adversarial Data Poisoning
Willsey, Max	Small Proofs from Congruence Closure
Wilson, Amalee	Strategies for Parallel SMT Solving
Wu, Haoze	Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers On Optimizing Back-Substitution Methods for Neural Network Verification On Optimizing Back-Substitution Methods for Neural Network Verification
Y
Yalcinkaya, Beyazit	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Yang, Suwei	INC: A Scalable Incremental Weighted Sampler Incremental Weighted Sampling
Yao, Xiaomo	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Yu, Emily	Stratified Certification for k-Induction
Z
Zelazny, Tom	On Optimizing Back-Substitution Methods for Neural Network Verification Verification-Aided Deep Ensemble Selection Verification-Driven Ensemble Selection On Optimizing Back-Substitution Methods for Neural Network Verification
Zhang, Min	Neural Network Verification with Proof Production Proof Production for Neural Network Verification
Zhang, Ruoxi	Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
Zhou, Xiang	Bounded Model Checking for LLVM

Disclaimer | Powered by EasyChair Smart Program