Research
Building programming languages, tools, and software engineering techniques that make software more reliable, secure, and productive.
Welcome to the inaugural lecture in the Dr. TLA+ Series! The presentation slide and the complete schedule of Dr. TLA+ Series are available at https://github.com/tlaplus/DrTLAPlus This lecture will familiarize you with the Paxos…
P is a programming framework for design, implementation, and validation of event-driven asynchronous systems. The P language incorporates deep modeling and specification techniques into asynchronous programming. It allows the programmer to systematically test and debug…
I will present our K-based language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as…
A collection of libraries to assist in the creation of PowerBI custom visuals. Projects Visual Utils (visual-utils) (opens in new tab) – A collection of utilities the development of powerbi custom visuals. Visual Settings (visual-settings)…
OPAL is a programming language and environment for designing intelligent assistants based on natural language. Tasks in OPAL can explore multiple hypothetical worlds to resolve the ambiguity in users’ intent by exploring its potential implications…
Note: This research project has reached its conclusion. These pages are maintained for reference and archival purposes. We are designing programming languages for building safe and reliable asynchronous systems. These languages are based on the programming…
The Checked C project is extending the C programming language so that programmers can write more secure and reliable C programs. The project is developing an extension to C called Checked C that adds checking…
IVy is a language and a tool for specifying, modeling, implementing and verifying protcols. IVy is intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing…
