Welcome to Software Foundations Laboratory!
- Our technique “Lightweight Verification of Separate Compilation” has been applied to CompCert 2.7.
Our research focuses on theoretically interesting software problems that are also practically useful.
Please see below for the details of our current projects.
- Formal Semantics of C (with weak memory model)
- Compiler Verification
- Probabilistic Programming
- Graduate Students
- Undergraduate Interns
- Former Members
Professor: Room 407 Bldg 301, TEL: 02-880-1844
Students: Room 416 Bldg 301, TEL: 02-880-4165