PROGRAM
Days: Monday, September 21st Tuesday, September 22nd Wednesday, September 23rd Thursday, September 24th
Monday, September 21st
View this program: with abstractssession overviewtalk overview
17:00-18:15 Session 1: Tutorial I: Alexander Nadel (all times are in CEST timezone - UTC+2)
17:00 | Anytime Algorithms for MaxSAT and Beyond (abstract) |
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
Chair:
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
19:05-20:00 Session 6: Invited talk I: Peter Schrammel
19:05 | How testable is business software? (abstract) |
20:00-20:55 Session 7: Software verification + learning
Chair:
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
Chair:
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
Chair:
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
19:05-20:00 Session 10: Invited Talk II: Orna Kupferman
19:05 | From Correctness to High Quality (abstract) |
Thursday, September 24th
View this program: with abstractssession overviewtalk overview
17:00-18:00 Session 12: SAT / SMT
Chair:
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
Chair:
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) |