FMCAD 2020: FORMAL METHODS IN COMPUTER AIDED DESIGN

A
Alizadeh Alamdari, Parand	Formal Methods with a Touch of Magic
Arif, M. Fareed	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Asadi, Sepideh	Incremental Verification by SMT-based Summary Repair
Avni, Guy	Formal Methods with a Touch of Magic
Azevedo de Amorim, Arthur	Automating Compositional Analysis of Authentication Protocols
B
Baier, Christel	SWITSS: Computing Small Witnessing Subsystems
Bansal, Chetan	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Barrett, Clark	Parallelization Techniques for Verifying Neural Networks A Theoretical Framework for Symbolic Quick Error Detection Reductions for Strings and Regular Expressions Revisited
Baumgartner, Jason	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Beame, Paul	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Biere, Armin	Tutorial on Word-Level Model Checking The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Blicha, Martin	Incremental Verification by SMT-based Summary Repair
Brauße, Franz	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
Bueno, Denis	EUFicient Reachability for Software with Arrays
C
Cauli, Claudia	Formal Threat Modeling in the Cloud
Chatterjee, Prantik	Distributed Bounded Model Checking
Chowdhury, Omar	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Cimatti, Alessandro	Reactive Synthesis from Extended Bounded Response LTL Specifications
Cook, Byron	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Cox, Arlen	EUFicient Reachability for Software with Arrays
D
D'Souza, Deepak	Specification Synthesis using Constrained Horn Clauses
Deisinger, Nate	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Devriendt, Jo	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Diep, Bui Phi	Distributed Bounded Model Checking
Doebel, Bjoern	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Dureja, Rohit	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
E
Echeverria, Mitziu	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Ehlers, Rüdiger	Learning Properties in LTL \cap ACTL from Positive Examples Only
Elboher, Yizhak	An Abstraction-Based Framework for Neural Network Verification
Elffers, Jan	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
F
Fedotov, Alexander	Effective System Level Liveness Verification
Fedyukovich, Grigory	Automating Modular Verification of Secure Information Flow Specification Synthesis using Constrained Horn Clauses Incremental Verification by SMT-based Summary Repair
Fleury, Mathias	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Fouladi, Sadjad	Parallelization Techniques for Verifying Neural Networks
Funke, Florian	SWITSS: Computing Small Witnessing Subsystems
G
Gavran, Ivan	Learning Properties in LTL \cap ACTL from Positive Examples Only
Geatti, Luca	Reactive Synthesis from Extended Bounded Response LTL Specifications
Georgiou, Pamina	Trace Logic for Inductive Loop Reasoning
Gigante, Nicola	Reactive Synthesis from Extended Bounded Response LTL Specifications
Gleiss, Bernhard	Trace Logic for Inductive Loop Reasoning
Gopinath, Divya	Parallelization Techniques for Verifying Neural Networks
Gopinath, Sridhar	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Gottschlich, Justin	An Abstraction-Based Framework for Neural Network Verification
Gupta, Aarti	Automating Modular Verification of Secure Information Flow
H
Harder, Hans	SWITSS: Computing Small Witnessing Subsystems
Henzinger, Thomas A.	Formal Methods with a Touch of Magic
Hyvärinen, Antti	Incremental Verification by SMT-based Summary Repair
I
Irfan, Ahmed	Parallelization Techniques for Verifying Neural Networks
J
Jagannathan, Suresh	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Jantsch, Simon	SWITSS: Computing Small Witnessing Subsystems
Jia, Limin	Automating Compositional Analysis of Authentication Protocols
Julian, Kyle	Parallelization Techniques for Verifying Neural Networks
K
Kanzelman, Robert	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Katz, Guy	Parallelization Techniques for Verifying Neural Networks An Abstraction-Based Framework for Neural Network Verification
Kaufmann, Daniela	The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Keiren, Jeroen J.A.	Effective System Level Liveness Verification
Khasidashvili, Zurab	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
Klimis, Vasileios	Model Checking Software-Defined Networks with Flow Entries that Time Out
Korovin, Konstantin	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
Kovacs, Laura	Trace Logic for Inductive Loop Reasoning
Kroening, Daniel	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Kugler, Hillel	Formal Verification for Natural and Engineered Biological Systems
Kumar, Rahul	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Kupferman, Orna	From Correctness to High Quality
L
Lahiri, Shuvendu	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Lal, Akash	Distributed Bounded Model Checking Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Larraz, Daniel	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Levin, Vladimir	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Lichtenberg, Jakob	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Liew, Vincent	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Lin, Xuankang	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Lonsing, Florian	A Theoretical Framework for Symbolic Quick Error Detection
Lukina, Anna	Formal Methods with a Touch of Magic
M
Madhukar, Kumar	Specification Synthesis using Constrained Horn Clauses
Manthey, Norbert	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Mitra, Subhasish	A Theoretical Framework for Symbolic Quick Error Detection
Montanari, Angelo	Reactive Synthesis from Extended Bounded Response LTL Specifications
Möhle, Sibylle	(Dual) Projected Propositional Model Counting and Enumeration without Repetition
N
Nadel, Alexander	Anytime Algorithms for MaxSAT and Beyond On Optimizing a Generic Function in SAT
Nagashima, Yutaka	Smart Induction for Isabelle/HOL (Tool Paper)
Namjoshi, Kedar	Modular Synthesis of Reactive Systems
Neider, Daniel	Learning Properties in LTL \cap ACTL from Positive Examples Only
Niemetz, Aina	Ternary Propagation-Based Local Search for More Bit-Precise Reasoning
Noetzli, Andres	Reductions for Strings and Regular Expressions Revisited
Nordstrom, Jakob	Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
Nutz, Alexander	Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
O
Ozdemir, Alex	Parallelization Techniques for Verifying Neural Networks
P
Pani, Thomas	Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction Thread-modular Counter Abstraction for Parameterized Program Safety
Parisis, George	Model Checking Software-Defined Networks with Flow Entries that Time Out
Pasareanu, Corina	Parallelization Techniques for Verifying Neural Networks Automating Compositional Analysis of Authentication Protocols
Pick, Lauren	Automating Modular Verification of Secure Information Flow
Pohlack, Martin	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Polgreen, Elizabeth	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Prabhu, Sumanth	Specification Synthesis using Constrained Horn Clauses
Preiner, Mathias	Ternary Propagation-Based Local Search for More Bit-Precise Reasoning
R
Reus, Bernhard	Model Checking Software-Defined Networks with Flow Entries that Time Out
Reynolds, Andrew	Reductions for Strings and Regular Expressions Revisited SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Roy, Subhajit	Distributed Bounded Model Checking
Rozier, Kristin Yvonne	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
S
Sahoo, Debashis	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
Sakallah, Karem A.	EUFicient Reachability for Software with Arrays
Samanta, Roopsha	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Schmaltz, Julien	Effective System Level Liveness Verification
Schrammel, Peter	How testable is business software?
Schuppe, Georg	Compositional Adviser-Strategy Synthesis for Multi-Agent Systems
Sharygina, Natasha	Incremental Verification by SMT-based Summary Repair
Skadron, Kevin	Runtime Verification on FPGAs with LTLf Specifications
T
Tabajara, Lucas	Runtime Verification on FPGAs with LTLf Specifications
Tautschnig, Michael	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Thakkar, Aalok	Modular Synthesis of Reactive Systems
Tinelli, Cesare	Reductions for Strings and Regular Expressions Revisited SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
Tonetta, Stefano	Reactive Synthesis from Extended Bounded Response LTL Specifications
Tracy II, Tommy	Runtime Verification on FPGAs with LTLf Specifications
Trefler, Richard	Modular Synthesis of Reactive Systems
V
Vardi, Moshe	Runtime Verification on FPGAs with LTLf Specifications
Vo, Daniella	Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease
W
Weissenbacher, Georg	Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction Thread-modular Counter Abstraction for Parameterized Program Safety
Wieczorkiewicz, Pawel	Using model checking tools to triage the severity of security bugs in the Xen hypervisor
Williams, Mark	Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Wu, Haoze	Parallelization Techniques for Verifying Neural Networks
Z
Zeljić, Aleksandar	Parallelization Techniques for Verifying Neural Networks
Zhang, Zichao	Automating Compositional Analysis of Authentication Protocols
Zhu, He	ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Zuleger, Florian	Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction Thread-modular Counter Abstraction for Parameterized Program Safety

Disclaimer | Powered by EasyChair Smart Program