Programming Languages & Software Engineering Research Projects
Validating Relational Database Systems at Scale via Learning-based Automated Testing
This research aims to fully automate the testing of relational database systems, focusing on test-case generation, reduction, and deduplication. By combining traditional and learning-based methods, the project seeks to improve testing efficiency. As part of our ongoing efforts, we have found more than 100 unique, previously unknown bugs in key systems.
Investigating Product Configuration as Knowledge Compilation
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.
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.
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.
Automated Verification for Imperative Higher-Order Programs
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.
Automated Proof Evolution for Verified Software Systems
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
Synthesis of Heap-Manipulating Programs from Separation Logic specifications
-
Computing 1
13 Computing Drive
Singapore 117417
© National University of Singapore. All Rights Reserved. • Legal • Branding guidelines