04 Sep 2019

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.

02 Aug 2019

Congrats to Drew, Ben Boskin, and Pete for the acceptance of their HCOMP paper Gamification of Loop-Invariant Discovery from Code!

17 Apr 2019

Congrats to Stavros on the acceptance of his CAV paper Automated Synthesis of Secure Platform Mappings!

17 Apr 2019

Congrats to Peizun and Thomas on the acceptance of their CAV paper Verifying asynchronous event-driven programs using partial abstract transformers!

17 Apr 2019

Congrats to Mitesh and Pete on the acceptance of their CAV paper Local and Compositional Reasoning for Optimized Reactive Systems!



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


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

NSF SaTC: CORE: Medium: Collaborative: Bridging the Gap Between Protocol Design and Implementation through Automated Mapping :

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