
Our mission is to make everyone a programmer and maximize the productivity of every programmer. This will democratize computing to empower every person and every organization to achieve more. We achieve our vision through open-ended fundamental research in programming languages, software engineering, and automated reasoning. We strongly believe in pushing our research to its logical extreme to positively impact people’s lives.
Foundations
Logical formalisms and theorem proving
Programming languages/models
Bosque (opens in new tab), Catala (opens in new tab), F* (opens in new tab), Koka (opens in new tab), TLA+ (opens in new tab)
High assurance/performance cloud
Correctness
Network Verification, Project Everest, Torch
AI and Big Data
Program analysis tools
Verifiers
Corral, Angelic Verification, Verisol
Program understanding/debugging
AI-assisted software development