OVERLAY 2025: 7TH INTERNATIONAL WORKSHOP ON ARTIFICIAL INTELLIGENCE AND FORMAL VERIFICATION, LOGIC, AUTOMATA, AND SYNTHESIS

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

A
Abstract Interpretation	Passive Learning of Lattice Automata from Recurrent Neural Networks
Accuracy	Verifiable Boosted Tree Ensembles
Adversarial Attack	Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties
Agda proof assistant	NAMOR: a New Agda Library for Modal Extended Sequents
Alignments	Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges
Ambiguity	A Proposal For Handling Query Ambiguity For Process Mining Tasks
Analytical models	Verifiable Boosted Tree Ensembles
Answer Set Programming	Scaling DRL Training via Symbolic Knowledge Transfer
Assume-guarantee reasoning	Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
Automata	Automata Cascades for Model Checking
Automata Learning	Fully Learnable Neural Reward Machines Passive Learning of Lattice Automata from Recurrent Neural Networks
Automated reasoning	Reasoning on Privacy Policies
B
boosted tree ensembles	Verifiable Boosted Tree Ensembles
BPM	Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges
Business Process Management	A Proposal For Handling Query Ambiguity For Process Mining Tasks
büchi automata	RNN Generalization to Omega-Regular Languages
C
Cascade Product	Automata Cascades for Model Checking
Categorical semantics	From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading
Causal Graphs	A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
Causal Graphs	A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
Chain-of-Thought (CoT)	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Circuit Complexity	Circuit Complexity Meets Discrete Ordinary Differential Equations: An Overview
Clinically relevant properties	Run-time verification of robot-assisted surgery using visual input
Compliance Checking	Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges
Computer Vision	Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties
Concept-based XAI	Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties
Controlled natural languages	Reasoning on Privacy Policies
Conversational Agents	A Proposal For Handling Query Ambiguity For Process Mining Tasks
cut elimination	NAMOR: a New Agda Library for Modal Extended Sequents
D
Data Recording	Towards Runtime Detection of Novel Traffic Situations
Decision trees	Verifiable Boosted Tree Ensembles
Deep Reinforcement Learning	Fully Learnable Neural Reward Machines
Distributed Protocols	First-Order Linear Temporal Logic for Testing Distributed Protocols
E
Ensemble learning	Verifiable Boosted Tree Ensembles
Ethical and Trustworthy AI	Verifying Memoryless Sequential Decision-making of Large Language Models
Explainable AI	Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning
Explainable AI (XAI)	Space Explanations of Neural Network Classification
Explainable Neural Network	Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties
extended-sequents	NAMOR: a New Agda Library for Modal Extended Sequents
F
Fairness	A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
Fairness	A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
False Positive	False Positives in Robustness Checking of Neural Networks
Few-shot prompting	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
First-Order Linear Temporal Logic	First-Order Linear Temporal Logic for Testing Distributed Protocols
formal explanation of AI	Space Explanations of Neural Network Classification
Formal Languages	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Formal Methods	On the Verification of ML Systems and Models False Positives in Robustness Checking of Neural Networks RLROM: Monitoring and Training Reinforcement Learning Agents using Signal Temporal Logic
Formal Specification	Towards Runtime Detection of Novel Traffic Situations
Formal Verification	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects Verifiable Boosted Tree Ensembles Reasoning on Privacy Policies
G
Games under Incomplete Information	Learning to Coordinate without Communication under Incomplete Information
Golog	Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus - Extended Abstract
I
Image segmentation	Run-time verification of robot-assisted surgery using visual input
Implicit Communication	Learning to Coordinate without Communication under Incomplete Information
Implicit Computational Complexity	Circuit Complexity Meets Discrete Ordinary Differential Equations: An Overview
Interpretability	Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning
Intuitionistic modalities	From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading
K
Knowledge Representation and Reasoning	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Knowledge Transfer	Scaling DRL Training via Symbolic Knowledge Transfer
L
Large Language Models	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects Verifying Memoryless Sequential Decision-making of Large Language Models
Large Language Models	A Proposal For Handling Query Ambiguity For Process Mining Tasks
length generalization	RNN Generalization to Omega-Regular Languages
linear temporal logic	RNN Generalization to Omega-Regular Languages
LLMs	Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges
Local Robustness Verification	False Positives in Robustness Checking of Neural Networks
Logic-based explanations of neural networks	Space Explanations of Neural Network Classification
M
Machine Learning	On the Verification of ML Systems and Models
Modal logic	Let the Music Flow Where the Modal Branches Lead NAMOR: a New Agda Library for Modal Extended Sequents
Model Checking	Automata Cascades for Model Checking Leveraging LLMs for Formal Software Requirements: Challenges and Prospects Verifying Memoryless Sequential Decision-making of Large Language Models
Monitoring	RLROM: Monitoring and Training Reinforcement Learning Agents using Signal Temporal Logic
Multi-agent reinforcement learning	Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
Music generation	Let the Music Flow Where the Modal Branches Lead
N
Natural language processing	Reasoning on Privacy Policies
neural network explanation	Space Explanations of Neural Network Classification
Neural Network Verification	False Positives in Robustness Checking of Neural Networks Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties
Neural Networks	Circuit Complexity Meets Discrete Ordinary Differential Equations: An Overview
Neuro-Symbolic RL	Scaling DRL Training via Symbolic Knowledge Transfer
Neurosymbolic learning	Fully Learnable Neural Reward Machines
Nondeterministic Domains	Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus - Extended Abstract
Normalisation theorems	From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading
Novel Traffic Situation Detection	Towards Runtime Detection of Novel Traffic Situations
O
Offline Monitoring	First-Order Linear Temporal Logic for Testing Distributed Protocols
omega-regular languages	RNN Generalization to Omega-Regular Languages
One-shot prompting	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Online Monitoring	First-Order Linear Temporal Logic for Testing Distributed Protocols
Optimization	Verifiable Boosted Tree Ensembles
Ordinary Differential Equations	Circuit Complexity Meets Discrete Ordinary Differential Equations: An Overview
P
Polynomials	Verifiable Boosted Tree Ensembles
Privacy policies	Reasoning on Privacy Policies
Probabilistic Logic	A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
Probabilistic Logic	A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
Process Mining	A Proposal For Handling Query Ambiguity For Process Mining Tasks
Program Execution	Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus - Extended Abstract
Prompt-Engineering	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
proof theory	NAMOR: a New Agda Library for Modal Extended Sequents
Proofs-as-programs	From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading
R
RAG	Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges
Reactive Synthesis	Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus - Extended Abstract
Recurrent Neural Networks	Passive Learning of Lattice Automata from Recurrent Neural Networks RNN Generalization to Omega-Regular Languages Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning
Reinforcement Learning	RLROM: Monitoring and Training Reinforcement Learning Agents using Signal Temporal Logic
Robot-assisted surgery	Run-time verification of robot-assisted surgery using visual input
robustness	Verifiable Boosted Tree Ensembles
Run-time verification	Run-time verification of robot-assisted surgery using visual input
Runtime Monitoring	Towards Runtime Detection of Novel Traffic Situations
S
Safety	Automata Cascades for Model Checking Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
Security	Verifiable Boosted Tree Ensembles
sequent calculus	NAMOR: a New Agda Library for Modal Extended Sequents
Shared-control Games	Learning to Coordinate without Communication under Incomplete Information
Shielding	Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
Signal Temporal Logic	RLROM: Monitoring and Training Reinforcement Learning Agents using Signal Temporal Logic
Situation Calculus	Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus - Extended Abstract
Software Requirements Engineering	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Software Requirements Specifications	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Strategic Reasoning	Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus - Extended Abstract
Structural Rules	A Proof System with Causal Labels (Part II): checking Counterfactual Fairness A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
Symbolic machine learning	Let the Music Flow Where the Modal Branches Lead
T
Theorem Proving	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects
Traffic Situations	Towards Runtime Detection of Novel Traffic Situations
Training	Verifiable Boosted Tree Ensembles
Trustworthy AI	Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties
V
Verification	On the Verification of ML Systems and Models
Verificationist epistemic logic	From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading
W
Weighted Finite Automata	Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning
Z
Zero-shot prompting	Leveraging LLMs for Formal Software Requirements: Challenges and Prospects

Disclaimer | Powered by EasyChair Smart Program