FMCAD 2020: FORMAL METHODS IN COMPUTER AIDED DESIGN
PROGRAM

Days: Monday, September 21st Tuesday, September 22nd Wednesday, September 23rd Thursday, September 24th

Monday, September 21st

View this program: with abstractssession overviewtalk overview

18:15-18:25Coffee Break
18:25-19:40 Session 2: Tutorial II: Hillel Kugler
18:25
Formal Verification for Natural and Engineered Biological Systems (abstract)
19:40-19:50Coffee Break
19:50-21:05 Session 3: Tutorial III: Armin Biere
19:50
Tutorial on Word-Level Model Checking (abstract)
Tuesday, September 22nd

View this program: with abstractssession overviewtalk overview

17:00-18:00 Session 4: Hardware Verification
Chair:
17:00
Effective System Level Liveness Verification (abstract)
17:15
Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration (abstract)
17:30
A Theoretical Framework for Symbolic Quick Error Detection (abstract)
17:45
Runtime Verification on FPGAs with LTLf Specifications (abstract)
18:00-18:55 Session 5: Software verification
18:00
Distributed Bounded Model Checking (abstract)
18:15
EUFicient Reachability for Software with Arrays (abstract)
18:30
Thread-modular Counter Abstraction for Parameterized Program Safety (abstract)
18:45
Incremental Verification by SMT-based Summary Repair (abstract)
18:55-19:05Coffee Break
20:00-20:55 Session 7: Software verification + learning
20:00
Reactive Synthesis from Extended Bounded Response LTL Specifications (abstract)
20:15
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces (abstract)
20:30
Learning Properties in LTL \cap ACTL from Positive Examples Only (abstract)
20:45
Automating Compositional Analysis of Authentication Protocols (abstract)
Wednesday, September 23rd

View this program: with abstractssession overviewtalk overview

17:00-18:00 Session 8: Verification and Neural Networks
17:00
Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation (abstract)
17:15
Parallelization Techniques for Verifying Neural Networks (abstract)
17:30
Formal Methods with a Touch of Magic (abstract)
17:45
ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks (abstract)
18:00-18:55 Session 9: Applied Verification
18:00
Automating Modular Verification of Secure Information Flow (abstract)
18:15
Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost (abstract)
18:30
Model Checking Software-Defined Networks with Flow Entries that Time Out (abstract)
18:40
Using model checking tools to triage the severity of security bugs in the Xen hypervisor (abstract)
18:55-19:05Coffee Break
Thursday, September 24th

View this program: with abstractssession overviewtalk overview

17:00-18:00 Session 12: SAT / SMT
17:00
Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning (abstract)
17:15
On Optimizing a Generic Function in SAT (abstract)
17:30
Ternary Propagation-Based Local Search for More Bit-Precise Reasoning (abstract)
17:45
Reductions for Strings and Regular Expressions Revisited (abstract)
18:00-19:00 Session 13: Student Forum
18:00
An Abstraction-Based Framework for Neural Network Verification (abstract)
18:05
(Dual) Projected Propositional Model Counting and Enumeration without Repetition (abstract)
18:10
Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction (abstract)
18:15
Specification Synthesis using Constrained Horn Clauses (abstract)
18:20
Compositional Adviser-Strategy Synthesis for Multi-Agent Systems (abstract)
18:25
Modular Synthesis of Reactive Systems (abstract)
18:30
Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease (abstract)
18:35
Formal Threat Modeling in the Cloud (abstract)
19:00-19:10Coffee Break
19:10-20:05 Session 14: Theory and theorem proving
19:10
SWITSS: Computing Small Witnessing Subsystems (abstract)
19:25
Smart Induction for Isabelle/HOL (Tool Paper) (abstract)
19:40
Trace Logic for Inductive Loop Reasoning (abstract)
19:55
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus (abstract)