Archie Mearns

Deep Stereo Matching for Real-Time Depth Estimation in Embedded Visual-SLAM

Undergraduate dissertation · 2026

Investigated the use of optimised deep learning-based stereo depth estimation models to improve dense reconstruction over traditional stereo matching algorithms in a real-time Visual-SLAM pipeline. Used TensorRT quantisation to optimise existing stereo matching models before comparing and evaluating on standard datasets (KITTI, Middlebury), real-world data, and downstream effect on SLAM and dense scene reconstruction quality. The best performing model was able to produce dense, high quality reconstructions in real-time using an optimised configuration that decreased latency by 23x at the expense of only 5-12% accuracy loss.

Simulacra

Project · 2024/25 · C#, WPF

Led a group of 7 students in a year long software engineering project for the National Decommissioning Centre(NDC) as the coursework for Software Engineering 1 and 2.

The NDC is equipped with a £1.6m marine simulator featuring immersive 300-degree displays powered by over 20 different computers. The simulator is used extensively in their work in decommissioning and in renewable energy R&D. However, there are lots of routine day to day operations the engineers require that are not natively supported by the simulator.

We designed and implemented a scene editor, using C# and WPF, for the marine simulator supporting easy and efficient editing of scene files including complex operations unsupported by the simulator.

My focuses in the project were in scene parsing, internal representation, collision detection, search and other backend development.

Guided the software development lifecycle, from requirements gathering, through implementation, testing, refactoring, regular client meetings for feedback, and performance/usability evaluation. The final system met all client requirements and implemented many additional features.

Modular and Extensible ATL-based Model Checking Tool

Internship · 2026 · C

Formal verification of Multi-Agent Systems (MAS) increasingly requires accommodating new classes of properties for model checking tasks. Much recent work involving model checking tasks involving epistemic attributes, cryptographic reasoning, bias awareness and others that often lack accommodation in existing model checking tools. In many cases, the burden for creating an entirely new tool from scratch to support a specific research project or prototype is too high. Existing model checking tools for MAS such as MCMAS and PRISM typically support a single logic and model checking tasks are restricted to the supported modalities and model checking algorithm. To the best of our knowledge, no known model checking tool supports a natively extensible modelling language.

We present a modular and extensible command-line model checker for MAS with a core built around Alternating-time Temporal Logic, but which is architected and designed to support extensions and prototyping. The formula language, modelling language and model checking algorithm are all designed to be extended independently through plugins without requiring modification of the core of the tool. The extensibility is demonstrated with two implemented plugins: a symbolic cryptography extension supporting verification of cryptographic protocols including Diffie-Hellman and Station-to-Station using the Dolev-Yao adversary model, and Bias-aware ATL (bATL) which maps variables to bias levels supporting reasoning about the influence of bias-sensitive attributes in decision processes.

Contributions

• An extensible agent-oriented modelling language which unextended is equivalent to Concurrent Game Structures(CGS) but written with agent-local states and actions, together with the compiler that translates model files into standard CGSs through reachability exploration.
• A plugin architecture supporting extension of the formula language, modelling language and model checking algorithm enabling quick implementation of research ideas without requiring modification to the tools core.
• Completed extensions for cryptographic protocol verification and bATL model checking and in progress extension supporting probabilistic ATL with rewards (rPATL) demonstrating ability to support varied and qualitatively distinct kinds of extensions within the same tool.

Biomimetic Implicit Communication for Distributed Multi-Robot Task Allocation Under Communication Constraint

Research · 2025

Traditional distributed coordination methods for multi-robot systems have extensive communication, however, many potential applications for multi-robot systems such as in disaster response or exploration can't assume reliable communication channels.

I designed a novel algorithm inspired by honey bee waggle-dance behaviour relying on local interaction for distributed task allocation in a multi-robot foraging scenario. As all communication is through local interaction, communication failures or unreliability have no effect on performance.

Implemented the G-Prim Allocation Auction algorithm as the state of art baseline and ran controlled experiments evaluating task completion efficiency under varied communication ranges.

Hetereogenous Robot Collaboration for Autonomous Fossil Collection

Coursework · 2024 · Python, ROS2, pyrobosim

Created a simulation using ROS2 and pyrobosim for a cooperative multi-robot system for the discovery and collection of fossils.

Comprised of an explorer robot and a collector robot in which the explorer moves faster and uses less battery that focuses on exploring an area using custom search patterns identifying both fossils and objects in the landscape. It then communicates to the collector robot which then goes to collect a fossil and brings it back to deposit it.

Both robots make use of automated battery management that will consider the battery required and how much is necessary to reach the charger for all movement planning.

Features:

• Battery management
• Random terrain generation
• Dynamic path planning
• Sensor simulation for object detection
• Exploration in custom search patterns