← Back to home

Publications

Forthcoming (2026)

Authenticated Data Structures for Trustworthy AI Agent Pipelines

Nasser Ali Alzahrani, James Harland, Maria Spichkova

ENASE 2026 · International Conference on Evaluation of Novel Approaches to Software Engineering

Characterizes the trust gap in AI agent-tool communication and proposes an ADS integration architecture. Demonstrates practical feasibility with the ADS4All framework, including empirical benchmarks showing sub-microsecond proof verification and minimal pipeline overhead.

Design Methodology and Lessons Learned from Building Generic Authenticated Data Structures in Mainstream Languages

Nasser Ali Alzahrani, James Harland, Maria Spichkova

ENASE 2026 · International Conference on Evaluation of Novel Approaches to Software Engineering

Presents a category-theoretic design methodology for implementing authenticated data structures in Haskell. Evaluates composition strategies, triangulated verification approaches, and performance-security trade-offs in production ADS implementations.

Published

Application of Property-based Testing Tools for Metamorphic Testing

Nasser Alzahrani, Maria Spichkova, James Harland

ENASE 2022 · pp. 553–560

Investigates the integration of property-based testing tools with metamorphic testing methodologies, demonstrating how QuickCheck-style generators can systematically derive metamorphic relations for functional programs.

ADS4all: Democratizing Authenticated Data Structures

Nasser Alzahrani, Ibrahim Khalil, Xun Yi

ICSOC 2019 · Springer · pp. 280–286

Introduces a framework for making authenticated data structures accessible to practitioners, enabling developers to build tamper-evident systems without deep cryptographic expertise.

Spatio-temporal Models for Formal Analysis and Property-Based Testing

Nasser Alzahrani, Maria Spichkova, Jan Olaf Blech

STAF 2016 · Springer · pp. 196–206

Develops spatio-temporal models for formal analysis and property-based testing of distributed systems, combining spatial reasoning with temporal logic for verification.