FLOC 2022: FEDERATED LOGIC CONFERENCE 2022
CAV PROGRAM

Days: Sunday, August 7th Monday, August 8th Tuesday, August 9th Wednesday, August 10th

Sunday, August 7th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 85A: Formal Methods for Probabilistic Programs
Location: Taub 1
09:00
Data-Driven Invariant Learning for Probabilistic Programs (abstract)
PRESENTER: Subhajit Roy
09:20
Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (abstract)
09:40
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (abstract)
PRESENTER: Lutz Klinkenberg
10:00
Abstraction-Refinement for Hierarchical Probabilistic Models (abstract)
PRESENTER: Sebastian Junges
10:30-11:00Coffee Break
11:00-12:00 Session 89: Keynote
11:00
Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (abstract)
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, ITP).

 

14:00-15:30 Session 90A: Formal Methods for Neural Networks
Location: Taub 1
14:00
Shared Certificates for Neural Network Verification (abstract)
14:20
Example Guided Synthesis of Linear Approximations for Neural Network Verification (abstract)
PRESENTER: Brandon Paulsen
14:40
Verifying Neural Networks Against Backdoor Attacks (abstract)
PRESENTER: Long H. Pham
15:00
Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning (abstract)
PRESENTER: Jiaxu Tian
15:20
Neural Network Robustness as a Verification Property: A Principled Case Study (abstract)
PRESENTER: Marco Casadio
15:30-16:00Coffee Break
16:00-17:30 Session 92A: Software Verification and Model Checking
Location: Taub 1
16:00
The Lattice-Theoretic Essence of Property Directed Reachability Analysis (abstract)
PRESENTER: Mayuko Kori
16:20
Affine Loop Invariant Generation via Matrix Algebra (abstract)
PRESENTER: Yucheng Ji
16:40
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (abstract)
17:00
Proof-guided Underapproximation Widening for Bounded Model Checking (abstract)
PRESENTER: Subhajit Roy
17:20
SolCMC: Solidity Compiler’s Model Checker (abstract)
PRESENTER: Leonardo Alt
Monday, August 8th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 94A: Hyperproperties and Security
Location: Taub 1
09:00
Software Verification of Hyperproperties Beyond k-Safety (abstract)
PRESENTER: Raven Beutner
09:20
A Scalable Shannon Entropy Estimator (abstract)
PRESENTER: Kuldeep S. Meel
09:40
PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (abstract)
PRESENTER: Yuxin Fan
10:00
Explaining Hyperproperty Violations (abstract)
PRESENTER: Julian Siber
10:20
Distilling Constraints in Zero-Knowledge Protocols (abstract)
PRESENTER: Miguel Isabel
10:30-11:00Coffee Break
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).

14:00-15:30 Session 97A: Formal Methods for Hardware, Cyber-Physical and Hybrid Systems
Location: Taub 1
14:00
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (abstract)
PRESENTER: Ryotaro Banno
14:20
Abstraction Modulo Stability for Reverse Engineering (abstract)
PRESENTER: Anna Becchi
14:40
Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (abstract)
PRESENTER: Ethan Lew
15:00
RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (abstract)
PRESENTER: Sylvie Putot
15:10
STLmc: Robust STL Model Checking of Hybrid Systems using SMT (abstract)
PRESENTER: Kyungmin Bae
15:20
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 98A: Probabilistic Techniques
Location: Taub 1
16:00
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (abstract)
16:20
Sampling-Based Verification of CTMCs with Uncertain Rates (abstract)
PRESENTER: Thom Badings
16:40
Playing Against Fair Adversaries in Stochastic Games with Total Rewards (abstract)
PRESENTER: Pablo Castro
17:00
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (abstract)
PRESENTER: Lorenz Leutgeb
17:20
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (abstract)
PRESENTER: Aina Niemetz
18:30-20:30 Walking tour (at Haifa)

pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)

Tuesday, August 9th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
10:30-11:00Coffee Break
11:00-12:30 Session 102A: Automata and Logic
Location: Taub 1
11:00
FORQ-based Language Inclusion Formal Testing (abstract)
PRESENTER: Kyveli Doveri
11:20
Sound Automation of Magic Wands (abstract)
11:40
Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (abstract)
PRESENTER: Yong Li
12:00
From Spot 2.0 to Spot 2.10: What's New? (abstract)
12:10
Complementing Büchi Automata with Ranker (abstract)
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).

13:00-14:00 Session 103: Tool Demonstrations

Tool demonstrations for:

  1. STLmc: Robust STL Model Checking of Hybrid Systems using SMT (13:00-13:30)
  2. UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (13:30-14:00)
14:00-16:00 Session 104A: Deductive Verification and Decision Procedures
Location: Taub 1
14:00
Even Faster Conflicts and Lazier Reductions for String Solvers (abstract)
PRESENTER: Andres Noetzli
14:20
Local Search For SMT on Linear Integer Arithmetic (abstract)
PRESENTER: Shaowei Cai
14:40
Reasoning about Data Trees using CHCs (abstract)
PRESENTER: Gennaro Parlato
15:00
Verified Erasure Correction in Coq with MathComp and VST (abstract)
PRESENTER: Joshua M. Cohen
15:20
End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (abstract)
PRESENTER: Shenghao Yuan
15:40
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (abstract)
PRESENTER: Joonwon Choi
16:00-16:30Coffee Break
16:30-17:30 Session 108: Plenary
Chair:
16:30
SMT-based Verification of Distributed Network Control Planes (abstract)
17:30-18:30 Session 109: Business Meeting

17:30-17:45 - As part of the buisneess meeting we will have a 15 minutes presentation by Pavithra Prabhakar.

Title: Formal Methods and Verification Programs and International Partnerships at NSF.

The talk will provide a brief overview of the funding opportunities at the US National Science Foundation related to the area of formal methods and computer aided verification. International partnerships and opportunities for participation of the broader scientific community will be highlighted.

Location: Taub 1
Wednesday, August 10th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
10:30-11:00Coffee Break
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, IJCAR, ITP).

13:00-14:00 Session 114: Tool Demonstrations

Tool demonstrations for:

  1. From Spot 2.0 to Spot 2.10: What's New? (13:00-13:30)
  2. Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (13:30-14:00)
14:00-15:30 Session 115A: Machine Learning
Location: Taub 1
14:00
Specification-Guided Learning of Nash Equilibria with High Social Welfare (abstract)
14:20
Synthesizing Fair Decision Trees via Iterative Constraint Solving (abstract)
PRESENTER: Jingbo Wang
14:40
SMT-based Translation Validation for Machine Learning Compiler (abstract)
PRESENTER: Juneyoung Lee
15:00
Verifying Fairness in Quantum Machine Learning (abstract)
PRESENTER: Ji Guan
15:20
MoGym: Using Formal Models for Training and Verifying Decision-making Agents (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 116A: Synthesis and Concurrency
Location: Taub 1
16:00
Synthesis and Analysis of Petri Nets from Causal Specifications (abstract)
16:20
Verifying generalised and structural soundness of workflow nets via relaxations (abstract)
16:40
Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (abstract)
PRESENTER: Andreas Katis
16:50
Information Flow Guided Synthesis (abstract)
PRESENTER: Niklas Metzger
17:10
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (abstract)
PRESENTER: Andreas Gittis