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
Chair:
Erika Abraham
Location: Taub 1
09:00
Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu and Subhajit Roy
Data-Driven Invariant Learning for Probabilistic Programs (abstract)
PRESENTER: Subhajit Roy
09:20
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer and Đorđe Žikelić
Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (abstract)
PRESENTER: Đorđe Žikelić
09:40
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (abstract)
PRESENTER: Lutz Klinkenberg
10:00
Sebastian Junges and Matthijs T. J. Spaan
Abstraction-Refinement for Hierarchical Probabilistic Models (abstract)
PRESENTER: Sebastian Junges
10:30-11:00Coffee Break
11:00-12:00 Session 89: Keynote
Chair:
Moshe Vardi
Location: Churchill Auditorium
11:00
Ziyad Hanna
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
Chair:
Pavithra Prabhakar
Location: Taub 1
14:00
Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin Vechev
Shared Certificates for Neural Network Verification (abstract)
PRESENTER: Dimitar I. Dimitrov
14:20
Brandon Paulsen and Chao Wang
Example Guided Synthesis of Linear Approximations for Neural Network Verification (abstract)
PRESENTER: Brandon Paulsen
14:40
Long H. Pham and Jun Sun
Verifying Neural Networks Against Backdoor Attacks (abstract)
PRESENTER: Long H. Pham
15:00
Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min Zhang
Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning (abstract)
PRESENTER: Jiaxu Tian
15:20
Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan Refaeli
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
Chair:
Supratik Chakraborty
Location: Taub 1
16:00
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga and Ichiro Hasuo
The Lattice-Theoretic Essence of Property Directed Reachability Analysis (abstract)
PRESENTER: Mayuko Kori
16:20
Yucheng Ji, Hongfei Fu, Bin Fang and Haibo Chen
Affine Loop Invariant Generation via Matrix Algebra (abstract)
PRESENTER: Yucheng Ji
16:40
Ahmed Bouajjani, Wael-Amine Boutglay and Peter Habermehl
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (abstract)
PRESENTER: Wael-Amine Boutglay
17:00
Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal and Subhajit Roy
Proof-guided Underapproximation Widening for Bounded Model Checking (abstract)
PRESENTER: Subhajit Roy
17:20
Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha Sharygina
SolCMC: Solidity Compiler’s Model Checker (abstract)
PRESENTER: Leonardo Alt
17:30-18:45 Session 93: Logic Lounge: Future of Autonomous Driving; Keynote by Shai Shalev-Shwartz (Mobileye and The Hebrew University of Jerusalem); Panel: Gila Kamhi (Intel, Haifa), Sanjit Seshia (UC Berkeley)
Chair:
Georg Weissenbacher
Location: Churchill Auditorium
19:00-20:30 FLoC Reception (at the Technion)
Location: Taub entrance floor / floor 1 lobbies
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
Chair:
Swen Jacobs
Location: Taub 1
09:00
Raven Beutner and Bernd Finkbeiner
Software Verification of Hyperproperties Beyond k-Safety (abstract)
PRESENTER: Raven Beutner
09:20
Priyanka Golia, Brendan Juba and Kuldeep S. Meel
A Scalable Shannon Entropy Estimator (abstract)
PRESENTER: Kuldeep S. Meel
09:40
Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei Liu
PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (abstract)
PRESENTER: Yuxin Fan
10:00
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger and Julian Siber
Explaining Hyperproperty Violations (abstract)
PRESENTER: Julian Siber
10:20
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez and Albert Rubio
Distilling Constraints in Zero-Knowledge Protocols (abstract)
PRESENTER: Miguel Isabel
10:30-11:00Coffee Break
11:00-12:30 Session 96A: Invited Talk: A Billion SMT Queries a Day (Neha Rungta)
Chair:
Alessandro Cimatti
Location: Taub 1
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
Chair:
Pierre Ganty
Location: Taub 1
14:00
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga and Kohei Suenaga
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (abstract)
PRESENTER: Ryotaro Banno
14:20
Anna Becchi and Alessandro Cimatti
Abstraction Modulo Stability for Reverse Engineering (abstract)
PRESENTER: Anna Becchi
14:40
Stanley Bak, Sergiy Bogomolov, Niklas Kochdumper, Ethan Lew and Kostiantyn Potomkin
Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (abstract)
PRESENTER: Ethan Lew
15:00
Eric Goubault and Sylvie Putot
RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (abstract)
PRESENTER: Sylvie Putot
15:10
Geunyeol Yu, Jia Lee and Kyungmin Bae
STLmc: Robust STL Model Checking of Hybrid Systems using SMT (abstract)
PRESENTER: Kyungmin Bae
15:20
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. Seshia
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (abstract)
PRESENTER: Elizabeth Polgreen
15:30-16:00Coffee Break
16:00-17:30 Session 98A: Probabilistic Techniques
Chair:
Joost-Pieter Katoen
Location: Taub 1
16:00
Chaitanya Agarwal, Shibashis Guha, Jan Křetínský and Pazhamalai Muruganandham
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (abstract)
PRESENTER: Chaitanya Agarwal
16:20
Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias Volk
Sampling-Based Verification of CTMCs with Uncertain Rates (abstract)
PRESENTER: Thom Badings
16:40
Pablo Castro, Pedro R. D'Argenio, Luciano Putruele and Ramiro Demasi
Playing Against Fair Adversaries in Stochastic Games with Total Rewards (abstract)
PRESENTER: Pablo Castro
17:00
Lorenz Leutgeb, Georg Moser and Florian Zuleger
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (abstract)
PRESENTER: Lorenz Leutgeb
17:20
Aina Niemetz, Mathias Preiner and Clark Barrett
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
09:00-10:30 Session 100A: CAV Award 2022
Chair:
Orna Grumberg
Location: Taub 1
10:30-11:00Coffee Break
11:00-12:30 Session 102A: Automata and Logic
Chair:
Nir Piterman
Location: Taub 1
11:00
Kyveli Doveri, Pierre Ganty and Nicolas Mazzocchi
FORQ-based Language Inclusion Formal Testing (abstract)
PRESENTER: Kyveli Doveri
11:20
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. Summers
Sound Automation of Magic Wands (abstract)
PRESENTER: Thibault Dardinier
11:40
Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun Zhang
Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (abstract)
PRESENTER: Yong Li
12:00
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard and Henrich Lauko
From Spot 2.0 to Spot 2.10: What's New? (abstract)
PRESENTER: Alexandre Duret-Lutz
12:10
Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková
Complementing Büchi Automata with Ranker (abstract)
PRESENTER: Barbora Šmahlíková
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)
Location: Taub entrance floor lobby
14:00-16:00 Session 104A: Deductive Verification and Decision Procedures
Chair:
Elizabeth Polgreen
Location: Taub 1
14:00
Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare Tinelli
Even Faster Conflicts and Lazier Reductions for String Solvers (abstract)
PRESENTER: Andres Noetzli
14:20
Shaowei Cai, Bohan Li and Xindi Zhang
Local Search For SMT on Linear Integer Arithmetic (abstract)
PRESENTER: Shaowei Cai
14:40
Marco Faella and Gennaro Parlato
Reasoning about Data Trees using CHCs (abstract)
PRESENTER: Gennaro Parlato
15:00
Joshua M. Cohen, Qinshi Wang and Andrew W. Appel
Verified Erasure Correction in Coq with MathComp and VST (abstract)
PRESENTER: Joshua M. Cohen
15:20
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel Baccelli
End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (abstract)
PRESENTER: Shenghao Yuan
15:40
Joonwon Choi, Adam Chlipala and Arvind
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:
Eran Yahav
Location: Churchill Auditorium
16:30
Aarti Gupta
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.

Chairs:
Sharon Shoham and Yakir Vizel
Location: Taub 1
19:30-22:00 FLoC Banquet (at Bikta Bayar - Beit Oren) - Paid event
Wednesday, August 10th

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

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 110A: CAV Award 2021
Chair:
Orna Grumberg
Location: Taub 1
10:30-11:00Coffee Break
11:00-12:30 Session 112A: Invited Talk: Program Verification with Constrained Horn Clauses (Arie Gurfinkel)
Chair:
Hadar Frenkel
Location: Taub 1
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)
Location: Taub entrance floor lobby
14:00-15:30 Session 115A: Machine Learning
Chair:
Caterina Urban
Location: Taub 1
14:00
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani and Rajeev Alur
Specification-Guided Learning of Nash Equilibria with High Social Welfare (abstract)
PRESENTER: Kishor Jothimurugan
14:20
Jingbo Wang, Yannan Li and Chao Wang
Synthesizing Fair Decision Trees via Iterative Constraint Solving (abstract)
PRESENTER: Jingbo Wang
14:40
Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung Lee
SMT-based Translation Validation for Machine Learning Compiler (abstract)
PRESENTER: Juneyoung Lee
15:00
Ji Guan, Wang Fang and Mingsheng Ying
Verifying Fairness in Quantum Machine Learning (abstract)
PRESENTER: Ji Guan
15:20
Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian Alexander Köhl and Verena Wolf
MoGym: Using Formal Models for Training and Verifying Decision-making Agents (abstract)
PRESENTER: Maximilian Alexander Köhl
15:30-16:00Coffee Break
16:00-17:30 Session 116A: Synthesis and Concurrency
Chair:
Marijana Lazic
Location: Taub 1
16:00
Mateus De Oliveira Oliveira
Synthesis and Analysis of Petri Nets from Causal Specifications (abstract)
16:20
Michael Blondin, Filip Mazowiecki and Philip Offtermatt
Verifying generalised and structural soundness of workflow nets via relaxations (abstract)
PRESENTER: Philip Offtermatt
16:40
Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger and Johann Schumann
Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (abstract)
PRESENTER: Andreas Katis
16:50
Bernd Finkbeiner, Niklas Metzger and Yoram Moses
Information Flow Guided Synthesis (abstract)
PRESENTER: Niklas Metzger
17:10
Andreas Gittis, Eric Vin and Daniel Fremont
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (abstract)
PRESENTER: Andreas Gittis