Foundations, algorithms, and tools for trustworthy computing.
We are the Foundations of Computer Systems Lab at the National University of Singapore, led by Umang Mathur and part of NUS PLSE. We develop programming languages, formal methods, and tools to make software and hardware more reliable.
Lab website · Research · Publications · People
| Direction | What we work on |
|---|---|
| Concurrent software | Finding and explaining concurrency bugs through race detection, predictive analysis, controlled testing, and linearizability monitoring. |
| Reliable and secure hardware | Languages, type systems, and verification for hardware. Anvil checks timing contracts to prevent timing hazards. Try it · Documentation. |
| Software translation | Preserving program behavior while moving code across languages, including C to safe Rust. Research · Collaborative projects. |
| Logic and automata | Algorithms, decidability, and machine-checked foundations. Trace theory in Lean formalizes Mazurkiewicz traces and recognizable trace languages. |
| Project | What you can do |
|---|---|
| RAPID | Analyse concurrent execution traces for data races, atomicity violations, and temporal properties. |
| GCT | Explore alternative goroutine schedules and replay failures in Go tests. |
| LinP | Check linearizability of complete, unambiguous histories for sets, stacks, queues, and priority queues. |
| Relational algebra in Lean | Prove program and relation equations with KA/KAT tactics. A Lean port and extension of Damien Pous's library. |
| Parikh's theorem in Lean | Work with a mechanized proof and a verified compiler from grammars to semilinear representations. |
| Compiler verification tutorial | Learn compiler correctness through a Lean port of Xavier Leroy's course, with proofs and exercises. |
For our work on ThreadSanitizer instrumentation, start with the experiment guide.
For questions about a tool, use its repository's issue tracker. For research collaborations or opportunities to join the lab, visit Umang's webpage and meet the team.
