Talk Keyword Index

TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

Shortcuts: A B C D E F G H I K L M N O P Q R S T U V W Z ω

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