Programming Languages & Software Engineering Research Projects

Investigating Product Configuration as Knowledge Compilation

Roland YAP

Industrial configuration problems suffer from slowness and a lack of real-world data. By merging Knowledge Compilation (KC) with practical configuration issues, this Tier 1 project aims to develop faster solvers.

Scalable, Precise and Configurable Neural Network Verification

KHOO Siau Cheng

This project proposes a novel platform for verifying neural networks (NNs), prioritizing scalability and precision. Unlike existing methods, it enables segmentation of NNs for applying varied verification techniques, enhancing configurability. Additionally, it investigates innovative approaches to boost verification accuracy while maintaining efficiency.

Deep Teaching-Improving Learning Outcomes with Advanced LMS

Martin HENZ, Boyd ANDERSON, LOW Kok Lim

The project aims to enhance a CS introductory course LMS (Source Academy @ NUS) by extending the system using programming language research and machine learning methods. This involves adding features such as improved program visualization, early detection of struggling students, and more helpful feedback on code.

• 
• Programming & Software Engineering Education

Source Academy

Martin HENZ, LOW Kok Lim, Sanka RASNAYAKA, Boyd ANDERSON

Source Academy is an immersive online experiential environment for introductory courses in computer science, used at NUS and Uppsala University. The system serves as a research platform for investigating the pedagogy of computational thinking and programming.

• 
• 
• 
• TRL 5
• Programming & Software Engineering Education

Automated Verification for Imperative Higher-Order Programs

CHIN Wei Ngan

This project aims to develop an automated verification solution for imperative higher-order programs, utilizing a novel specification logic called Staged Separation Logic (SSL). The research addresses questions related to SSL's handling of closures and general recursions/iterators, its ability to verify programs rejected by Rust's type systems, and the efficiency of solving proof obligations.

Practical Automated Testing of Distributed Systems

Ilya SERGEY

• TRL 4

Automated Proof Evolution for Verified Software Systems

Ilya SERGEY

This project automates proof evolution for verified software systems, adapting proofs to changing specs and programs. It emphasizes Separation Logic, aiming to advance beyond proof-of-concept stage for real-world systems.

SuSLik

Ilya SERGEY

Synthesis of Heap-Manipulating Programs from Separation Logic specifications

• 
• Program Logics & Semantics, Program Synthesis

Fuzz Testing

Abhik ROYCHOUDHURY

• 
• TRL 4
• Software Testing

Automated Program Repair

Abhik ROYCHOUDHURY

• 
• 
• 
• TRL 4
• Program Repair