Overall Objectives
Research Program
- Symbolic verification of cryptographic applications
- Computational verification of cryptographic applications
- F*: A Higher-Order Effectful Language for Program Verification
- Efficient Formally Secure Compilers to a Tagged Architecture
- Provably secure web applications
- Design and Verification of next-generation protocols: identity, blockchains, and messaging
Application Domains
New Software and Platforms
New Results
Bilateral Contracts and Grants with Industry
Partnerships and Cooperations
Bibliography
Overall Objectives
Research Program
- Symbolic verification of cryptographic applications
- Computational verification of cryptographic applications
- F*: A Higher-Order Effectful Language for Program Verification
- Efficient Formally Secure Compilers to a Tagged Architecture
- Provably secure web applications
- Design and Verification of next-generation protocols: identity, blockchains, and messaging
Application Domains
New Software and Platforms
New Results
Bilateral Contracts and Grants with Industry
Partnerships and Cooperations
Bibliography