FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

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

Disclaimer | Powered by EasyChair Smart Program