Publications

A complete list of my publications across formal methods, control theory and AI verification.

For citation metrics, see my Google Scholar profile — the homepage also carries an automatically updating list of my papers scraped from Google Scholar.

Conference

[C20] Safe Control of Semi-Explicit Differential-Algebraic Systems: Control Barrier Functions with SOS Verification

Mohamad H. Kazma, Hongchao Zhang, Abdallah A. Albustami, Ben Wooding, Meiyi Ma, Taylor T. Johnson, Ahmad F. Taha

IEEE Conference on Decision and Control (CDC), 2026 (to appear)
[C19] Safe Autonomous Takeover for Unknown Descriptor Systems

Ben Wooding, Mohamad H. Kazma, Hongchao Zhang, Ahmad F. Taha, Meiyi Ma, Taylor T. Johnson

IEEE Conference on Decision and Control (CDC), 2026 (to appear)
[C18] Control Barrier Function Synthesis for Differential-Algebraic Systems

Hongchao Zhang, Mohamad H. Kazma, Ben Wooding, Meiyi Ma, Taylor T. Johnson, Ahmad F. Taha

IEEE Conference on Decision and Control (CDC), 2026 (to appear)
[C17] NNV3: Expanding Neural Network Verification to New Architectures and Domains

Anne Marie Tumlin^*, Samuel Sasaki^*, Ben Wooding, Diego Manzanas Lopez, Muhammad Usama Zubair, Navid Hashemi, Hongchao Zhang, Waseem Abbas, Ipek Oguz, Meiyi Ma, Taylor T. Johnson

International Symposium on Automated Technology for Verification and Analysis (ATVA), 2026 (to appear; ^*co-first authors)
[C16] ARCH-COMP26 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

Luca Geretti, Julien Alexandre dit Sandretto, Matthias Althoff, Luis Benet, Pieter Collins, Marcelo Forets, Stefan Mitsch, Mark Perschl, Christian Schilling, Jorge Tillet, Ben Wooding

13th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH), 2026 (authors alphabetical)

PDF · easychair.org
[C15] ARCH-COMP26 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

Samuel Sasaki^*, Ben Wooding^*, Matthias Althoff, Luis Benet, Samuel Coogan, Marcelo Forets, Akash Harapanahalli, Lukas Koller, Tobias Ladner, Christian Schilling, Taylor T. Johnson, Hongchao Zhang, Xiangru Zhong

13th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH), 2026 (^*category co-leads)

PDF · easychair.org
[C14] k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

Ben Wooding, Hongchao Zhang, Taylor T. Johnson, Abolfazl Lavaei

3rd International Conference on Neuro-Symbolic Systems (NeuS), 2026 (selected as oral presentation — 28% of submissions)

PDF · arXiv:2605.20108
[C13] MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts Architecture

Quang Pham, Ben Wooding, Luke Nam, Samuel Sasaki, Taylor T. Johnson

9th International Symposium on AI Verification (SAIV), 2026

PDF · DOI
[C12] Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features

Anne Marie Tumlin, Ben Wooding, Zhenxuan Shao, Diego Manzanas Lopez, Tyler Derr, Taylor T. Johnson

9th International Symposium on AI Verification (SAIV), 2026

PDF · DOI
[C11] A Self-Correcting Neuro-Symbolic AI Reasoning Framework

Ben Wooding^*, Kiersten Brennan^*, Anne Marie Tumlin, Hongchao Zhang, Taylor T. Johnson

9th International Symposium on AI Verification (SAIV), 2026 (^*contributed equally)

PDF · DOI
[C10] ARCH-COMP25 Category Report: Stochastic Models

Alessandro Abate, Omid Akbarzadeh, Henk A. P. Blom, Sofie Haesaert, Sina Hassani, Abolfazl Lavaei, Frederik Baymler Mathiesen, Rahul Misra, Amy Nejati, Mathis Niehage, Fie Ørum, Anne Remke, Behrad Samari, Ruohan Wang, Rafael Wisniewski, Ben Wooding, Mahdieh Zaker

12th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH25), 2025 (authors alphabetical)

PDF · DOI · arXiv:2506.17602
[C9] Proving the Correctness of CANDO3 Optrode Command Interface VDM model in Isabelle/HOL

Leo Freitas, Ben Wooding, Bill Scott, Andrew Pollitt, Patrick Degenaar

23rd Overture Workshop and 3rd INTO-CPS Association Brainstorm, 2025

PDF · www.overturetool.org
[C8] TRUST: Stability and Safety Controller Synthesis for Unknown Dynamical Models Using a Single Trajectory

Jamie Gardner^*, Ben Wooding^*, Amy Nejati, Abolfazl Lavaei

Hybrid Systems: Computation and Control (HSCC), 2025 (^*contributed equally)

PDF · DOI
[C7] PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems

Ben Wooding, Viacheslav Horbanov, Abolfazl Lavaei

International Colloquium on Theoretical Aspects of Computing (ICTAC), 2025 [2^nd place — ARCH 2025 Best Result Award]

PDF · DOI
[C6] Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

Oliver Schön, Shammakh Naseer, Ben Wooding, Sadegh Soudjani

Analysis and Design of Hybrid Systems (ADHS), 2024

PDF · DOI
[C5] IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems

Ben Wooding, Abolfazl Lavaei

Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), 2024

PDF · DOI
[C4] Robust Simulation Functions with Disturbance Refinement

Ben Wooding, Abolfazl Lavaei, Vahid Vahidinasab, Sadegh Soudjani

European Control Conference (ECC), 2023

PDF · DOI
[C3] Tuning Robotti: the machine-assisted exploration of parameter spaces in multi-models of a cyber-physical system

Sergiy Bogomolov, John Fitzgerald, Frederik F. Foldager, Carl Gamble, Peter Gorm Larsen, Kenneth Pierce, Paulius Stankaitis, Ben Wooding

18th International Overture Workshop, 2021 (authors alphabetical)

PDF · arXiv:2101.07261 · www.overturetool.org
[C2] ARCH-COMP20 Category Report: Stochastic Models

Alessandro Abate, Henk Blom, Nathalie Cauchi, Joanna Delicaris, Arnd Hartmanns, Mahmoud Khaled, Abolfazl Lavaei, Carina Pilch, Anne Remke, Stefan Schupp, Fedor Shmarov, Sadegh Soudjani, Abraham Vinod, Ben Wooding, Majid Zamani, Paolo Zuliani

7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020 (authors alphabetical)

PDF · DOI
[C1] Formal Controller Synthesis for Frequency Regulation Utilising Electric Vehicles

Ben Wooding, Vahid Vahidinasab, Sadegh Soudjani

Smart Energy Systems and Technologies (SEST), 2020

PDF · DOI

Journal

[J2] A logic-based resilience metric for water resource recovery facilities

Anna S. Laino, Ben Wooding, Sadegh Soudjani, Russell J. Davenport

Environmental Science: Water Research & Technology, 2025 [1 of 20 papers (8.5% of eligible papers) chosen for the themed collection — Highlights from Environmental Science: Water Research & Technology in 2024]

PDF · DOI
[J1] Data-Driven Abstraction-Based Control Synthesis

Milad Kazemi^*, Rupak Majumdar, Mahmoud Salamati^*, Sadegh Soudjani, Ben Wooding^*

Nonlinear Analysis: Hybrid Systems (NAHS), 2024 (^*contributed equally)

PDF · DOI

Book Chapters

[B3] Cyber-Physical Smart Homes/Buildings

Ben Wooding, Vahid Vahidinasab, Milad Kazemi, Sadegh Soudjani

Cyber-Physical Structures of Power Applications, 2025

PDF · salford-repository.worktribe.com
[B2] Control and management of active buildings

Ben Wooding, Vahid Vahidinasab, Milad Kazemi, Sadegh Soudjani

Active Building Energy Systems: Operation and Control, 2021

PDF · DOI
[B1] Operation and control of a population of active buildings at network level

Ben Wooding, Vahid Vahidinasab, Sadegh Soudjani

Active Building Energy Systems: Operation and Control, 2021

PDF · DOI

Posters & Competition Contributions

[M3] n2v: Neural Network Verification in Python (Competition Contribution)

Samuel Sasaki, Ben Wooding, Hanchen D. Wang, Anne Marie Tumlin, Meiyi Ma, Taylor T. Johnson

9th International Symposium on AI Verification (SAIV), 2026

PDF · DOI
[M2] Poster Abstract: PRoTECT: Parallel Construction of Barrier Certificates for Safety Verification of Polynomial Systems

Ben Wooding, Viacheslav Horbanov, Abolfazl Lavaei

International Conference on Cyber-Physical Systems (ICCPS), 2025 [2^nd place — ARCH 2025 Best Result Award]

PDF · DOI
[M1] Poster Abstract: IMPaCT: A Parallelized Software Tool for IMDP Construction and Controller Synthesis with Convergence Guarantees

Ben Wooding, Abolfazl Lavaei

Hybrid Systems: Computation and Control (HSCC), 2024

PDF · DOI

Theses

[T2] Model-Based and Data-Driven Formal Synthesis of Power Systems

Ben Wooding

PhD thesis, School of Computing, Newcastle University, 2023

PDF · theses.ncl.ac.uk
[T1] Using Formal Methods and Proof to Verify a CANDO Epilepsy Medical Device

Ben Wooding

MComp dissertation, Newcastle University, 2019

PDF

Preprints (under review)

[P11] Benchmark: Formal Verification for Surgical Robots

Jamie Fong, Ben Wooding, Taylor T. Johnson

Under submission, 2026
[P10] Composing Multi-Agent Behavior Trees

Jamie Fong, Ben Wooding, Taylor T. Johnson

Under submission, 2026
[P9] From Estimation to Detection: Sequential Change Detection for Alignment Monitoring

Samuel Sasaki, Ben Wooding, Anthony J. Clark, Taylor T. Johnson

Under submission, 2026
[P8] Learning Reach-Set Geometry for Tighter Probabilistic Neural Network Verification

Samuel Sasaki, Ben Wooding, Taylor T. Johnson

Under submission, 2026
[P7] BehaVerify: A Formal Verification Tool for Behavior Trees

Serena S. Serbinowska, Ben Wooding, Diego Manzanas Lopez, Luke Nam, Anne Marie Tumlin, Nicholas K. Potteiger, Hongchao Zhang, Taylor T. Johnson

Under submission, 2026
[P6] Roger? Probabilistic Certificates for Safety-Critical ATC Speech Recognition

Ben Wooding, Taylor T. Johnson

Under submission, 2026
[P5] Control Barrier Certificates for Unknown Linear Differential-Algebraic Equation Systems

Ben Wooding, Mohamad H. Kazma, Hongchao Zhang, Meiyi Ma, Ahmad F. Taha, Taylor T. Johnson

Under submission, 2026
[P4] Robust Simulation Functions for Interconnected Systems under Large Disturbances

Ben Wooding, Sadegh Soudjani

Under submission, 2026
[P3] Input-Agnostic Probabilistic Neural Network Verification for Vision, Speech and Depth

Ben Wooding, Anne Marie Tumlin, Samuel Sasaki, Hongchao Zhang, Taylor T. Johnson

Under submission, 2026
[P2] Learning k-Inductive Control Barrier Certificates for Unknown Nonlinear Dynamics Beyond Polynomials

Ben Wooding, Abolfazl Lavaei

Under submission, 2024

arXiv:2412.07232
[P1] Formal Control of New England 39-Bus Test System: An Assume-Guarantee Approach

Ben Wooding, Abolfazl Lavaei, Sadegh Soudjani

arXiv preprint, 2023

arXiv:2307.03467

Publications

Conference

[C20] Safe Control of Semi-Explicit Differential-Algebraic Systems: Control Barrier Functions with SOS Verification

[C19] Safe Autonomous Takeover for Unknown Descriptor Systems

[C18] Control Barrier Function Synthesis for Differential-Algebraic Systems

[C17] NNV3: Expanding Neural Network Verification to New Architectures and Domains

[C16] ARCH-COMP26 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

[C15] ARCH-COMP26 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

[C14] k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

[C13] MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts Architecture

[C12] Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features

[C11] A Self-Correcting Neuro-Symbolic AI Reasoning Framework

[C10] ARCH-COMP25 Category Report: Stochastic Models

[C9] Proving the Correctness of CANDO3 Optrode Command Interface VDM model in Isabelle/HOL

[C8] TRUST: Stability and Safety Controller Synthesis for Unknown Dynamical Models Using a Single Trajectory

[C7] PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems

[C6] Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

[C5] IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems

[C4] Robust Simulation Functions with Disturbance Refinement

[C3] Tuning Robotti: the machine-assisted exploration of parameter spaces in multi-models of a cyber-physical system

[C2] ARCH-COMP20 Category Report: Stochastic Models

[C1] Formal Controller Synthesis for Frequency Regulation Utilising Electric Vehicles

Journal

[J2] A logic-based resilience metric for water resource recovery facilities

[J1] Data-Driven Abstraction-Based Control Synthesis

Book Chapters

[B3] Cyber-Physical Smart Homes/Buildings

[B2] Control and management of active buildings

[B1] Operation and control of a population of active buildings at network level

Posters & Competition Contributions

[M3] n2v: Neural Network Verification in Python (Competition Contribution)

[M2] Poster Abstract: PRoTECT: Parallel Construction of Barrier Certificates for Safety Verification of Polynomial Systems

[M1] Poster Abstract: IMPaCT: A Parallelized Software Tool for IMDP Construction and Controller Synthesis with Convergence Guarantees

Theses

[T2] Model-Based and Data-Driven Formal Synthesis of Power Systems

[T1] Using Formal Methods and Proof to Verify a CANDO Epilepsy Medical Device

Preprints (under review)

[P11] Benchmark: Formal Verification for Surgical Robots

[P10] Composing Multi-Agent Behavior Trees

[P9] From Estimation to Detection: Sequential Change Detection for Alignment Monitoring

[P8] Learning Reach-Set Geometry for Tighter Probabilistic Neural Network Verification

[P7] BehaVerify: A Formal Verification Tool for Behavior Trees

[P6] Roger? Probabilistic Certificates for Safety-Critical ATC Speech Recognition

[P5] Control Barrier Certificates for Unknown Linear Differential-Algebraic Equation Systems

[P4] Robust Simulation Functions for Interconnected Systems under Large Disturbances

[P3] Input-Agnostic Probabilistic Neural Network Verification for Vision, Speech and Depth

[P2] Learning k-Inductive Control Barrier Certificates for Unknown Nonlinear Dynamics Beyond Polynomials

[P1] Formal Control of New England 39-Bus Test System: An Assume-Guarantee Approach