Programming Languages & Software Engineering
Software consists of programs written in programming languages.
The flexibility and power of software enables billions of people around the world to connect, collaborate, and solve problems.
However, as one of the most complex artifacts designed by humans, it is theoretically challenging and practically difficult to correctly program software.
We study all aspects of the software development process, with the aim to improve the performance and reliability of these programs.
What We Do
Study the foundational and theoretical aspects of programming languages and software engineering, exploring ways to improve program writing, as well as demonstrating the ‘correctness’ of programs.
Explore practical and implemental aspects of programming languages, software engineering, and software education, developing tools and systems to improve software quality and security.
Sub Areas
- Compilers
- Concurrency
- Constraint & Logic Programming
- Decision Procedures
- Formal Methods
- Functional Programming
- Language-Based Security
- Probabilistic Programming
- Program Analysis
- Program Logics & Semantics
- Program Repair
- Program Synthesis
- Programming & Software Engineering Education
- Software Security
- Software Testing
- Types
- Verification
Our Research Projects
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.
Scalable, Precise and Configurable Neural Network Verification
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
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
- Program Logics & Semantics, Program Synthesis
Our Research Groups
Verified Systems Engineering
We do research in the design and implementation of programming languages (PL), mathematical models of computation, and computer-assisted formal reasoning. We investigate the theoretical foundations of programming and build tools for ensuring that certain kinds of costly software errors and vulnerabilities never occur in the real-world code, which many people rely upon in their everyday lives.
- Compilers, Concurrency, Formal Methods, Functional Programming, Program Analysis, Program Logics & Semantics, Program Repair, Program Synthesis, Types, Verification
STeAdS Virtual Group
Software Engineering and Technological Advancements for Society. A virtual group that uses Software engineering practices and Technological advancements (Cloud computing, Artificial Intelligence (EdgeAI, ML)) for the benefit of various aspects of society (healthcare, education, art & culture). Looking for students to collaborate on different projects. Look at ganeshniyer.github.io for details.
- Programming & Software Engineering Education, Types
NUS Test Lab
The Trustworthy Engineering of Software Technologies (TEST) Lab is working on practical and conceptual software solutions. We aim to have a real-world impact both by creating practical tools as well as by designing principled, fundamental techniques.
- Compilers, Program Analysis, Programming & Software Engineering Education
