Finding Bugs in Randomised Software with Incorrectness Logic
Project ID: 2531bd1645
(You will need this ID for your application)
Research Theme: Information and Communication Technologies
Research Area(s):
verification and correctness
theoretical computer science
software engineering
UCL Lead department: Computer Science
Lead Supervisor: Quang Loc Le
Project Summary:
Randomised algorithms are crucial in modern applications such as machine learning, cryptography, bioinformatics, and data mining. However, the randomness in these algorithms complicates the prevention and detection of bugs. Traditional debugging methods, such as unit testing, symbolic execution, and fuzzing, are often ineffective in dealing with the non-determinism inherent in such programs. They may produce inconsistent test executions, leading developers to dismiss failures unintentionally. As such, developers frequently hardwire random seeds to enforce determinism, assuming test failures due to randomness rather than actual bugs. This common practice significantly increases the risk of missing critical errors.
This project aims to study a version of incorrectness logic with novel logical foundations and analysis techniques that can formally prove the presence of bugs in randomised software. This research aims to realise the idea through the following three key tasks. i) Analyse the types of bugs in real-world randomised software. ii) Propose Randomised Incorrectness Logic (RIL) that can model and reason about bugs in randomised software. It involves formalising the semantics of randomised programs, an assertion language that serves as an analogy to incorrectness logic, and an associated proof system. iii) Develop a bi-abduction technique for automatically inferring program specifications and compositional bug reporting with manifest bug definitions for randomised programs. It will also involve the iterative development of robust software prototypes and their experimental evaluation against the state-of-the-art.
The PhD will provide training in programming principles, logic, and formal verification. Candidates should have a Bachelor’s degree in computer science or mathematics. Ideal candidates should have a Master’s degree with a solid technical background and interest in programming languages and logical methods in computer science.
Supervisory Team: Quang Loc Le, James Brotherston, and Peter O’Hearn