This project explores how specialised programming frameworks called Guardrails, developed specifically for constraining large language models (LLMs), can prevent them from generating harmful, biased, or off-topic content. The goal of the project is to build simple examples using three leading guardrail frameworks implemented in Python: Guardrails AI, NeMo Guardrails from NVIDIA, and Llama Guard from … full description “A Comparative Analysis of Guardrail Frameworks for Large Language Models (available)”
Category: Programming Languages
Building a Benchmark Suite for Modal Mu-Calculus (available)
The modal mu-calculus [1] is a logic for expressing properties of abstract state transition systems, and generalises other logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Because of this, it is a very useful tool for describing and verifying the behaviour of computer systems. The aim of this project is to support … full description “Building a Benchmark Suite for Modal Mu-Calculus (available)”
Cyclist: Verifying Programs using Cyclic Proof (available)
Cyclic proofs are a technique for proving properties inductively, or proving properties about inductively defined objects or processes. They can be used to prove logical statements, or to verify recursive programs. The Cyclist tool [1] has been developed as an automatic verification tool based on cyclic proofs. It can prove termination and verify temporal properties … full description “Cyclist: Verifying Programs using Cyclic Proof (available)”
Deciding Isomorphism for Infinite Descent Problems (available)
The Infinite Descent property underpins two very important applications in program verification: termination of programs [1,2], on the one hand, and correctness of cyclic proofs of formulas or properties [3], on the other. In both cases, the object of interest (i.e. a program or a proof) is converted into an abstract form for which the … full description “Deciding Isomorphism for Infinite Descent Problems (available)”
Detecting broken security in hybrid Android apps (completed)
Many modern Android applications make use of a webview – a component providing easy access to the rendering engine and JavaScript interpreter of a full browser. The content shown by a webview can be loaded from a local resource or a remote server via HTTP and integrates seamlessly with the app. Webviews are popular with developers, … full description “Detecting broken security in hybrid Android apps (completed)”
Disassembling x86 binaries for static analysis and reverse engineering (completed)
The Jakstab static analyser for binaries automatically disassembles x86 binaries for Windows or Linux and reconstructs a control flow graph. It is particularly effective on targets that have been obfuscated with various tricks that throw off regular disassemblers such as IDA Pro. Jakstab disassembles one instruction at a time, translates it into an intermediate language, and then … full description “Disassembling x86 binaries for static analysis and reverse engineering (completed)”
Eclipse plugin for the ART parser generator (completed)
The ART parser generator is one of a new breed of compiler generation tools which provides efficient generalised parsing. This means that language designers have complete freedom to specify syntax in a way that supports downstream processes rather than having to shoehorn their ideas into the constraints imposed by current near-deterministic parser generators like Bison … full description “Eclipse plugin for the ART parser generator (completed)”
Embeded programming for INTI (available)
We are building a low-power transputer (parallel computer with microcontrollers) to study neuromorphic computing and run inference in low power devices (low power as in low computing power and low energy consumption). It is named the Incipient Neuromorphic Transputer Initiatiave in honour of Inti the Inca sun god. And because it is an incipient effort … full description “Embeded programming for INTI (available)”
Empirical evaluation of static verifiers for the Go programming language (available)
Go is a language that natively supports many constructs to synchronise concurrent threads. Because of this, developing code that contains subtle concurrency bugs is rather common. To address this problem, several groups of researchers have put forwards tools to find concurrency bugs in Go codebases. The objective of this project is to evaluate how some … full description “Empirical evaluation of static verifiers for the Go programming language (available)”
Formal semantics and C (completed)
When we want to know how a programming language construct such as Java exception handling works, we look it up in the language manual or a textbook. This is good enough for most programmers since they can test their understanding by compiling short programs and watching their effects in a debugger. However, compiler developers have … full description “Formal semantics and C (completed)”
Formalising Recursive Adaptive Grammars using a Proof Assistant (available)
The aim of this project is to formalise using proof assistant (such as Rocq [1], Agda [4], or Isabelle [5]) the meta-theory of the recursive adaptive grammar framework [2] Programming languages are usually specified on two levels. The first level defines a context-free grammar that specifies the syntax of the language. Usually, however, not all … full description “Formalising Recursive Adaptive Grammars using a Proof Assistant (available)”
Improving Automatic Bug Detection in JavaScript (completed)
Dynamic symbolic execution (DSE) is an effective tool for bug detection in real software. Like unit testing and fuzzing DSE executes portions of a program, exposing bugs through runtime program exceptions. In DSE, some inputs to the program under test are made “symbolic” while the rest are fixed. Whenever the symbolic execution encounters a conditional operation … full description “Improving Automatic Bug Detection in JavaScript (completed)”
Mechanisation of subtyping for Go 1.18 (available)
Go 1.18 [1] has recently been released. This new version includes generics and more flexible interfaces. Generics allow programmers to define data structures and functions that work safely for several types, e.g., like List<E> in Java which defines lists that can store any value of type E, where E is any type (String, Boolean, etc). … full description “Mechanisation of subtyping for Go 1.18 (available)”
Multiverse Debugging for Verilog (available)
Verilog is the most used hardware-description language: it is the primary language in which chips—from small microcontrollers to large SoCs and AI accelerators—are designed, simulated, and verified before being committed to silicon. Despite Verilog’s centrality in hardware development, its semantics is surprisingly poorly understood and the language is known for its many quirks. My recent … full description “Multiverse Debugging for Verilog (available)”
Verifying real-world concurrent Rust crates (available)
Rust is a popular systems programming language which enforces memory and thread safety through compile-time safety checks [1]. While these constraints effectively prevent data races in safe Rust code, verification of concurrent Rust programs remains an ongoing challenge. Concurrency bugs may occur for a number of reasons, including atomicity violations, “unsafe” Rust code and interactions … full description “Verifying real-world concurrent Rust crates (available)”