The aim of this project is to formalise within the Coq proof assistant [1] 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 syntactically correct programs make sense, and … full description “Coq Formalisation of Recursive Adaptive Grammars (available)”
Category: Programming Languages
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)”
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)”
Embedded firmware development for the Open Bot Brain project (available)
Software is a vital part of our infrastructure. You may be familiarwith software running on computers and phones. But software runs onmany more devices as part of an embedded microcontroller in thedevice, software running on embedded devices is often called firmware.Examples range from toothbrushes, to appliances, to tools, and devicesin the so called internet of … full description “Embedded firmware development for the Open Bot Brain project (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)”
Engineering ROTOR: a Refactoring Tool for OCaml (ongoing)
OCaml [1] is a mature functional programming language with an expressive type system. Recently, we have developed a prototype tool, called ROTOR, for automatically refactoring OCaml codebases [2]. Currently, ROTOR handles renaming of functions. This is surprisingly hard due to OCaml’s powerful module system: renaming a function in one module may actually require renaming functions … full description “Engineering ROTOR: a Refactoring Tool for OCaml (ongoing)”
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)”
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)”
Machine Learning Library for OCaml (completed)
Frameworks for machine learning include Python’s TensorFlow [1]. These frameworks provide standard ways of specifying models that can be optimised by machine learning algorithms. OCaml [2] is a mature functional programming language with an expressive type system. DecML [3] is a prototype OCaml extension that facilitates implementing machine learning tasks, based on specifying models as … full description “Machine Learning Library for OCaml (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)”
Parikh’s Theorem for Symbolic Register Automata (available)
Parikh’s Theorem is a fundamental result in automata theory with numerous applications in computer science. These include software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases), among others. Parikh’s Theorem states that the … full description “Parikh’s Theorem for Symbolic Register Automata (available)”
REST API and web frontend for a JavaScript symbolic testing framework (completed)
ExpoSE.js is a symbolic testing framework being developed at Royal Holloway designed to assist developers in improving the security and reliability of JavaScript applications, a language for which traditional software testing solutions have failed to produce satisfactory results. Symbolic execution is a technique which allows for the systematic enumeration of feasible paths of a program. … full description “REST API and web frontend for a JavaScript symbolic testing framework (completed)”
Smart IDE for Cascading Style Sheets in Web Development (completed)
You will construct an experimental IDE to aid programmers in writing Cascading Style Sheets (CSS) for web applications. Style sheets dictate how a web page appears, and consist of a series of rules which are applied to elements of the web page. Determining exactly which rule should be applied to which element is not entirely … full description “Smart IDE for Cascading Style Sheets in Web Development (completed)”
Visitors for Generalized Algebraic Data Types in OCaml (completed)
Algebraic datatypes (ADTs) [1] are the basic method for defining how to build complex data values in functional programming languages: they specify both the basic, or atomic, values, as well as the constructors for building larger values out of smaller ones. For example, the following ADT defines generic lists that contain values of type ‘a … full description “Visitors for Generalized Algebraic Data Types in OCaml (completed)”
Working on computer mediated artwork with the Tate Gallery (completed)
The Tate Gallery owns a set of major artworks which are computer mediated; that is they employ computers to manage interaction with gallery visitors in a variety of often technically challenging ways. We are working with the conservators at the Tate to document these systems and to think about managing their future in the long … full description “Working on computer mediated artwork with the Tate Gallery (completed)”