FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

A
Agarwal, Chaitanya	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Albert, Elvira	Distilling Constraints in Zero-Knowledge Protocols (, talk)
Alt, Leonardo	SolCMC: Solidity Compiler’s Model Checker (, talk)
Alur, Rajeev	Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Amir, Guy	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Appel, Andrew W.	Verified Erasure Correction in Coq with MathComp and VST (, talk)
Arvind,	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
B
Baccelli, Emmanuel	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Badings, Thom	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Bae, Kyungmin	STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Bak, Stanley	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Bang, Seongwon	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Banno, Ryotaro	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Bansal, Suguman	Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Bao, Jialu	Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Barbosa, Haniel	Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Barrett, Clark	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Bastani, Osbert	Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Becchi, Anna	Abstraction Modulo Stability for Reverse Engineering (, talk)
Bellés-Muñoz, Marta	Distilling Constraints in Zero-Knowledge Protocols (, talk)
Besson, Frédéric	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Beutner, Raven	Software Verification of Hyperproperties Beyond k-Safety (, talk)
Bian, Song	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Blicha, Martin	SolCMC: Solidity Compiler’s Model Checker (, talk)
Blondin, Michael	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Bogomolov, Sergiy	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Bouajjani, Ahmed	Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Boutglay, Wael-Amine	Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
C
Cai, Shaowei	Local Search For SMT on Linear Integer Arithmetic (, talk)
Casadio, Marco	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Castro, Pablo	Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Chatterjee, Krishnendu	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Chatterjee, Prantik	Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Cheang, Kevin	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Chen, Haibo	Affine Loop Invariant Generation via Matrix Algebra (, talk)
Chen, Mingshuai	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Chen, Taolue	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Chlipala, Adam	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Choi, Joonwon	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Chun, Inwhan	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Cimatti, Alessandro	Abstraction Modulo Stability for Reverse Engineering (, talk)
Coenen, Norine	Explaining Hyperproperty Violations (, talk)
Cohen, Joshua M.	Verified Erasure Correction in Coq with MathComp and VST (, talk)
Colange, Maximilien	From Spot 2.0 to Spot 2.10: What's New? (, talk)
D
D'Argenio, Pedro R.	Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Dachselt, Raimund	Explaining Hyperproperty Violations (, talk)
Daggitt, Matthew L.	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Dardinier, Thibault	Sound Automation of Magic Wands (, talk)
De Oliveira Oliveira, Mateus	Synthesis and Analysis of Petri Nets from Causal Specifications (, talk)
Demasi, Ramiro	Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Dimitrov, Dimitar I.	Shared Certificates for Neural Network Verification (, talk)
Doveri, Kyveli	FORQ-based Language Inclusion Formal Testing (, talk)
Dubois, Jérôme	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Duret-Lutz, Alexandre	From Spot 2.0 to Spot 2.10: What's New? (, talk)
F
Faella, Marco	Reasoning about Data Trees using CHCs (, talk)
Fan, Yuxin	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Fang, Bin	Affine Loop Invariant Generation via Matrix Algebra (, talk)
Fang, Wang	Verifying Fairness in Quantum Machine Learning (, talk)
Feng, Weizhi	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Finkbeiner, Bernd	Software Verification of Hyperproperties Beyond k-Safety (, talk) Explaining Hyperproperty Violations (, talk) Information Flow Guided Synthesis (, talk)
Fischer, Marc	Shared Certificates for Neural Network Verification (, talk)
Fremont, Daniel	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Frenkel, Hadar	Explaining Hyperproperty Violations (, talk)
Fu, Hongfei	Affine Loop Invariant Generation via Matrix Algebra (, talk)
G
Gaddamadugu, Pranav	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Ganty, Pierre	FORQ-based Language Inclusion Formal Testing (, talk)
Gbaguidi Aisse, Alexandre	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Giannakopoulou, Dimitra	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Gillard, Clément	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Gittis, Andreas	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Godbole, Adwait	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Goharshady, Amir Kafshdar	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Golia, Priyanka	A Scalable Shannon Entropy Estimator (, talk)
Goubault, Eric	RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Gros, Timo P.	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Guan, Ji	Verifying Fairness in Quantum Machine Learning (, talk)
Guha, Shibashis	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Gurfinkel, Arie	Program Verification with Constrained Horn Clauses (Invited Paper) ()
H
H. Pham, Long	Verifying Neural Networks Against Backdoor Attacks (, talk)
Habermehl, Peter	Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
Hahn, Christopher	Explaining Hyperproperty Violations (, talk)
Hasuo, Ichiro	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Havlena, Vojtěch	Complementing Büchi Automata with Ranker (, talk)
Hencey, Brandon	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Hermanns, Holger	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Hoffmann, Joerg	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Horak, Tom	Explaining Hyperproperty Violations (, talk)
Hsu, Justin	Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Hym, Samuel	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Hyvärinen, Antti	SolCMC: Solidity Compiler’s Model Checker (, talk)
I
Isabel, Miguel	Distilling Constraints in Zero-Knowledge Protocols (, talk)
J
Jansen, Nils	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Jhoo, Ho Young	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Ji, Yucheng	Affine Loop Invariant Generation via Matrix Algebra (, talk)
Jin, Peng	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Jothimurugan, Kishor	Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Juba, Brendan	A Scalable Shannon Entropy Estimator (, talk)
Junges, Sebastian	Abstraction-Refinement for Hierarchical Probabilistic Models (, talk) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
K
Katis, Andreas	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Katoen, Joost-Pieter	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Katsumata, Shin-ya	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Katz, Guy	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Klauck, Michaela	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Klinkenberg, Lutz	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Kochdumper, Niklas	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Kokke, Wen	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Komendantskaya, Ekaterina	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Kori, Mayuko	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Köhl, Maximilian Alexander	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Křetínský, Jan	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
L
Laeufer, Kevin	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Lal, Akash	Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Lauko, Henrich	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Lee, Jia	STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Lee, Juneyoung	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Lengal, Ondrej	Complementing Büchi Automata with Ranker (, talk)
Leutgeb, Lorenz	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Lew, Ethan	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Li, Bohan	Local Search For SMT on Linear Integer Arithmetic (, talk)
Li, Yannan	Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Li, Yong	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Lin, Shaokai	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Liu, Wanwei	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
M
Manerkar, Yatin A.	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Martin, Antoine	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Matsumoto, Naoki	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Matsuoka, Kotaro	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Mavridou, Anastasia	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Mazowiecki, Filip	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Mazzocchi, Nicolas	FORQ-based Language Inclusion Formal Testing (, talk)
Meda, Jaydeepsinh	Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Medioni, Thomas	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Meel, Kuldeep S.	A Scalable Shannon Entropy Estimator (, talk)
Meggendorfer, Tobias	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Metzger, Niklas	Explaining Hyperproperty Violations (, talk) Information Flow Guided Synthesis (, talk)
Mora, Federico	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Moser, Georg	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Moses, Yoram	Information Flow Guided Synthesis (, talk)
Muruganandham, Pazhamalai	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Müller, Peter	Sound Automation of Magic Wands (, talk)
N
Nam, Seunghyeon	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Niemetz, Aina	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
Noetzli, Andres	Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
O
Offtermatt, Philip	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
P
Parlato, Gennaro	Reasoning about Data Trees using CHCs (, talk)
Parthasarathy, Gaurav	Sound Automation of Magic Wands (, talk)
Pathak, Drashti	Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Paulsen, Brandon	Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Polgreen, Elizabeth	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Potomkin, Kostiantyn	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Preiner, Mathias	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
Pressburger, Thomas	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Putot, Sylvie	RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Putruele, Luciano	Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
R
Refaeli, Idan	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Renault, Etienne	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Renkin, Florian	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Reynolds, Andrew	Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Rodríguez-Núñez, Clara	Distilling Constraints in Zero-Knowledge Protocols (, talk)
Roy, Subhajit	Data-Driven Invariant Learning for Probabilistic Programs (, talk) Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Rubio, Albert	Distilling Constraints in Zero-Knowledge Protocols (, talk)
Rungta, Neha	A Billion SMT Queries a Day ()
S
Schlehuber-Caissier, Philipp	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Schumann, Johann	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Seshia, Sanjit A.	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
Sharygina, Natasha	SolCMC: Solidity Compiler’s Model Checker (, talk)
Siber, Julian	Explaining Hyperproperty Violations (, talk)
Singh, Gagandeep	Shared Certificates for Neural Network Verification (, talk)
Song, Fu	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Spaan, Matthijs T. J.	Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Sprecher, Christian	Shared Certificates for Neural Network Verification (, talk)
Stoelinga, Marielle	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Suenaga, Kohei	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Summers, Alexander J.	Sound Automation of Magic Wands (, talk)
Sun, Jun	Verifying Neural Networks Against Backdoor Attacks (, talk)
T
Talpin, Jean-Pierre	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Tian, Jiaxu	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Tinelli, Cesare	Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Trivedi, Nitesh	Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Turrini, Andrea	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
U
Urabe, Natsuki	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
V
Vardi, Moshe	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Vechev, Martin	Shared Certificates for Neural Network Verification (, talk)
Vin, Eric	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Volk, Matthias	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
W
Waga, Masaki	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Wang, Chao	Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Wang, Jingbo	Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Wang, Qinshi	Verified Erasure Correction in Coq with MathComp and VST (, talk)
Weeks, Noé	Sound Automation of Magic Wands (, talk)
Wen, Xuejun	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Winkler, Tobias	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Wolf, Verena	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Y
Ying, Mingsheng	Verifying Fairness in Quantum Machine Learning (, talk)
Yu, Geunyeol	STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Yuan, Shenghao	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Z
Zandberg, Koen	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
Zhang, Liangfeng	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Zhang, Lijun	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Zhang, Min	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Zhang, Xindi	Local Search For SMT on Linear Integer Arithmetic (, talk)
Zhi, Dapeng	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Zuleger, Florian	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Š
Šmahlíková, Barbora	Complementing Büchi Automata with Ranker (, talk)
Ž
Žikelić, Đorđe	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)

Disclaimer | Powered by EasyChair Smart Program