FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

A
abstraction and refinement	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Abstraction-Refinement	Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Actual Causality	Explaining Hyperproperty Violations (, talk)
adversarial robustness	Shared Certificates for Neural Network Verification (, talk)
Adversarial Training	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
amortised cost analysis	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Assume-Guarantee Synthesis	Information Flow Guided Synthesis (, talk)
Automata	Reasoning about Data Trees using CHCs (, talk)
Automated Testing	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
automatic verification	Sound Automation of Magic Wands (, talk)
automation	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
B
backdoor attack	Verifying Neural Networks Against Backdoor Attacks (, talk)
Bounded model checking	Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Büchi automata	FORQ-based Language Inclusion Formal Testing (, talk) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk) Complementing Büchi Automata with Ranker (, talk)
C
cache coherence	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
category theory	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
combining decision procedures	Reasoning about Data Trees using CHCs (, talk)
Compiler verification	SMT-based Translation Validation for Machine Learning Compiler (, talk)
complementation	Complementing Büchi Automata with Ranker (, talk)
Completeness guarantees	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Compositional Synthesis	Information Flow Guided Synthesis (, talk)
Constrained Horn Clauses	SolCMC: Solidity Compiler’s Model Checker (, talk) Reasoning about Data Trees using CHCs (, talk)
Constraint simplification	Distilling Constraints in Zero-Knowledge Protocols (, talk)
constraint solving	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
continuous reachability	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Controller Synthesis	Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Coq	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
correct-by-construction	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Counterexamples	Explaining Hyperproperty Violations (, talk)
Counterfactual Reasoning	Explaining Hyperproperty Violations (, talk)
D
data logics	Reasoning about Data Trees using CHCs (, talk)
Data-driven invariant learning	Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Data-driven methods	Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
decision tree	Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Deep Learning Compiler	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Deep reinforcement learning	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk)
Denotational semantics	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Determinization	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Distributed Synthesis	Information Flow Guided Synthesis (, talk)
Distributed Systems	Information Flow Guided Synthesis (, talk)
Divide-and-Conquer	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
domain-specific language	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
E
Emerson-Lei acceptance	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Emerson-Lei automata	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
Entropy Estimation	A Scalable Shannon Entropy Estimator (, talk)
Ethereum	SolCMC: Solidity Compiler’s Model Checker (, talk)
Explanations	Explaining Hyperproperty Violations (, talk)
F
fairness	Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
Fairness Verification	Verifying Fairness in Quantum Machine Learning (, talk)
Farkas' Lemma	Affine Loop Invariant Generation via Matrix Algebra (, talk)
fault isolation	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
fixed point theory	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
formal methods	MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
formal verification	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
free-choice nets	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Functional correctness verification	Verified Erasure Correction in Coq with MathComp and VST (, talk)
functional programming	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Fuzz Testing	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
G
games	Reasoning about Data Trees using CHCs (, talk)
generalized soundness	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Generating functions	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
H
hardware	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
Hierarchical Models	Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
homomorphic encryption	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Hyperliveness	Software Verification of Hyperproperties Beyond k-Safety (, talk)
HyperLTL	Software Verification of Hyperproperties Beyond k-Safety (, talk)
Hyperproperties	Software Verification of Hyperproperties Beyond k-Safety (, talk) Explaining Hyperproperty Violations (, talk)
I
Information Flow	Information Flow Guided Synthesis (, talk)
Information leakage	A Scalable Shannon Entropy Estimator (, talk)
inherently weak automata	Complementing Büchi Automata with Ranker (, talk)
Inner-approximation	RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Integer Difference Logic	Local Search For SMT on Linear Integer Arithmetic (, talk)
Interactive theorem proving	Verified Erasure Correction in Coq with MathComp and VST (, talk)
Internet of Things	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
Invariant synthesis	Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
K
Koopman operator	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
L
Language inclusion	FORQ-based Language Inclusion Formal Testing (, talk)
lattice theory	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Linear Approximation	Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Linear Bounding	Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Linear Integer Arithmetic	Local Search For SMT on Linear Integer Arithmetic (, talk)
Local Search	Local Search For SMT on Linear Integer Arithmetic (, talk)
local verification	Shared Certificates for Neural Network Verification (, talk)
Loop Invariant Generation	Affine Loop Invariant Generation via Matrix Algebra (, talk)
LTL	From Spot 2.0 to Spot 2.10: What's New? (, talk)
M
Machine Learning Compiler	SMT-based Translation Validation for Machine Learning Compiler (, talk)
magic wand	Sound Automation of Magic Wands (, talk)
Markov decision processes	Abstraction-Refinement for Hierarchical Probabilistic Models (, talk) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
Martingales	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Matrix Algebra	Affine Loop Invariant Generation via Matrix Algebra (, talk)
Mazurkiewicz Traces	Synthesis and Analysis of Petri Nets from Causal Specifications (, talk)
Mean payoff	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk)
model checking	Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning (, talk) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk) Explaining Hyperproperty Violations (, talk) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Model counting	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Model-Checking	Software Verification of Hyperproperties Beyond k-Safety (, talk)
monadic second-order logic	Reasoning about Data Trees using CHCs (, talk)
MSC Languages	Synthesis and Analysis of Petri Nets from Causal Specifications (, talk)
multi-modal verification	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
N
Neural network	Verifying Neural Networks Against Backdoor Attacks (, talk)
Neural Network Verification	Shared Certificates for Neural Network Verification (, talk) Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
Neural Networks	Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk)
Neural networks verification	RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Non-linear constraints	Distilling Constraints in Zero-Knowledge Protocols (, talk)
O
online LTL monitoring	Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (, talk)
P
Parametric continuous-time Markov chains	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Parity automata	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
petri nets	Synthesis and Analysis of Petri Nets from Causal Specifications (, talk) Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
polynomial zonotopes	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Predicate Abstraction	Software Verification of Hyperproperties Beyond k-Safety (, talk)
Probabilistic model checking	Abstraction-Refinement for Hierarchical Probabilistic Models (, talk) Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
probabilistic programming	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
Probabilistic programs	Data-Driven Invariant Learning for Probabilistic Programs (, talk) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk) Abstraction-Refinement for Hierarchical Probabilistic Models (, talk)
Program equivalence	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Program verification	Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (, talk)
proof assistants	Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (, talk)
proof methodology	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
property directed reachability analysis	The Lattice-Theoretic Essence of Property Directed Reachability Analysis (, talk)
Q
Quantified Information Flow	A Scalable Shannon Entropy Estimator (, talk)
Quantitative Synthesis	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Quantitative verification	Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (, talk)
Quantum Decision Model	Verifying Fairness in Quantum Machine Learning (, talk)
Quantum Machine Learning	Verifying Fairness in Quantum Machine Learning (, talk)
Quantum Noise	Verifying Fairness in Quantum Machine Learning (, talk)
R
R1CS	Distilling Constraints in Zero-Knowledge Protocols (, talk)
Rabin automata	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
random Fourier features	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk)
Randomized Planning	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
Reachability analysis	Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (, talk) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Realizability Checking	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
Reductions	Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Reed-Solomon coding	Verified Erasure Correction in Coq with MathComp and VST (, talk)
Reinforcement Learning	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Requirements Analysis	Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (, talk)
reverse engineering	Abstraction Modulo Stability for Reverse Engineering (, talk)
Robustness	Neural Network Robustness as a Verification Property: A Principled Case Study (, talk) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (, talk)
Robustness degree	STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
Robustness Verification	Example Guided Synthesis of Linear Approximations for Neural Network Verification (, talk)
S
Satisfiability Modulo Theories	SolCMC: Solidity Compiler’s Model Checker (, talk) Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Satisfiability Modulo Theory	SMT-based Translation Validation for Machine Learning Compiler (, talk)
Scenario optimization	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Secure Multi-Party Computation	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Security Policy	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
Security Verification	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk)
self-adjusting data structures	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (, talk)
semi-deterministic automata	Complementing Büchi Automata with Ranker (, talk)
separation logic	Sound Automation of Magic Wands (, talk)
Shannon Entropy	A Scalable Shannon Entropy Estimator (, talk)
Signal temporal logic	STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk)
simulations	Abstraction Modulo Stability for Reverse Engineering (, talk)
SMT	STLmc: Robust STL Model Checking of Hybrid Systems using SMT (, talk) Local Search For SMT on Linear Integer Arithmetic (, talk)
SMT solvers	Reasoning about Data Trees using CHCs (, talk)
SMT Solving	Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (, talk)
Software Verification	Proof-guided Underapproximation Widening for Bounded Model Checking (, talk) Software Verification of Hyperproperties Beyond k-Safety (, talk) Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Solidity	SolCMC: Solidity Compiler’s Model Checker (, talk)
soundness	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
stability	Abstraction Modulo Stability for Reverse Engineering (, talk)
Statistical Model Checking	PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (, talk) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (, talk)
Statistical Verification	Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk)
Stochastic Games	Playing Against Fair Adversaries in Stochastic Games with Total Rewards (, talk)
Stochastic invariants	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
Strings	Even Faster Conflicts and Lazier Reductions for String Solvers (, talk)
Strongly Connected Components	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (, talk)
structural soundness	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Symbolic Model Checking	SolCMC: Solidity Compiler’s Model Checker (, talk)
Synthesis	PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (, talk) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk) Specification-Guided Learning of Nash Equilibria with High Social Welfare (, talk) Synthesizing Fair Decision Trees via Iterative Constraint Solving (, talk)
T
Termination	Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (, talk)
tool	From Spot 2.0 to Spot 2.10: What's New? (, talk)
transformation	From Spot 2.0 to Spot 2.10: What's New? (, talk)
Translation validation	SMT-based Translation Validation for Machine Learning Compiler (, talk)
U
Uncertainty	Sampling-Based Verification of CTMCs with Uncertain Rates (, talk)
Underapproximation widening	Proof-guided Underapproximation Widening for Bounded Model Checking (, talk)
Uniform Random Sampling	Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (, talk)
V
Verification	Verifying Neural Networks Against Backdoor Attacks (, talk) Neural Network Robustness as a Verification Property: A Principled Case Study (, talk) Software Verification of Hyperproperties Beyond k-Safety (, talk) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (, talk)
virtual machines	End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (, talk)
W
Weakest pre-expectations	Data-Driven Invariant Learning for Probabilistic Programs (, talk)
Well-quasiorders	FORQ-based Language Inclusion Formal Testing (, talk)
workflow nets	Verifying generalised and structural soundness of workflow nets via relaxations (, talk)
Z
ZK protocols	Distilling Constraints in Zero-Knowledge Protocols (, talk)
ω
ω-automata	From Spot 2.0 to Spot 2.10: What's New? (, talk)

Disclaimer | Powered by EasyChair Smart Program