News
Congrats to Yijia for his successful defense of his thesis, Preserving Numerical Program Properties under Computing Uncertainties!
Congrats to Justin for his successful defense of his thesis, A Typed Programming Language: The Semantics of Rank Polymorphism!
Congrats to Peizun for his successful defense of his thesis, Resource-Aware Program Analysis using Observation Sequences!
Welcome to our new PhD students, Josh and Max! Josh will be working with Pete, and Max will be working with Stavros and Cristina Nita-Rotaru.
Congrats to Drew, Ben Boskin, and Pete for the acceptance of their HCOMP paper Gamification of Loop-Invariant Discovery from Code!
Congrats to Stavros on the acceptance of his CAV paper Automated Synthesis of Secure Platform Mappings!
Congrats to Peizun and Thomas on the acceptance of their CAV paper Verifying asynchronous event-driven programs using partial abstract transformers!
Congrats to Mitesh and Pete on the acceptance of their CAV paper Local and Compositional Reasoning for Optimized Reactive Systems!
People
Alumni
Yijia Gu
- PhD (2021)
-
Preserving Numerical Program Properties under Computing Uncertainties
Justin Slepak
- PhD (2020)
- Facebook
A Typed Programming Language: The Semantics of Rank Polymorphism
Peizun Liu
- PhD (2019)
- Google
Resource-Aware Program Analysis using Observation Sequences
Mitesh Jain
- PhD (2018)
- Synopsis
Refinement-Based Reasoning of Optimized Reactive Systems
Jaideep Ramachandran
- PhD (2018)
- Intel
From the Approximate to the Exact: Solving Floating-Point Formulas via Proxy Theories
Harsh Raju Chamarthi
- PhD (2016)
- Intel
Interactive Non-theorem Disproving
Vasilis Papavasileiou
- PhD (2015)
- Ocsigen
Mathematical Programming Modulo Theories
Peter Dillinger
- PhD (2010)
- Facebook
Adaptive Approximate State Storage
Projects
ACL2s : A powerful theorem prover.
CID: Confidentiality and Integrity of Deep Neural Networks : Protecting DNNs against attacks targeting the internal structure or the inference process
Compilation-Dependent Security Properties of Software : Detecting, fixing, and preventing information leaks (such as through side channels) introduced by security-ignorant compilers
Platform Dependencies of Floating-Point Programs : They give rise to inconsistencies across compilers and hardware. How much freedom should your compiler have?
Resource-Aware Program Verification using Observation Sequences : Analysis techniques for programs designed for variable amounts of some resource