research
∙
11/04/2022
This is not the End: Rethinking Serverless Function Termination
Elastic scaling is one of the central benefits provided by serverless pl...
share
research
∙
05/13/2022
Blockaid: Data Access Policy Enforcement for Web Applications
Modern web applications serve large amounts of sensitive user data, acce...
research
∙
10/30/2021
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Inferring inductive invariants is one of the main challenges of formal v...
research
∙
06/02/2021
Phoenix: A Formally Verified Regenerating Vault
An attacker that gains access to a cryptocurrency user's private keys ca...
research
∙
06/02/2021
Some Complexity Results for Stateful Network Verification
In modern networks, forwarding of packets often depends on the history o...
research
∙
06/02/2021
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Various verification techniques for temporal properties transform tempor...
research
∙
05/17/2021
Summing Up Smart Transitions
Some of the most significant high-level properties of currencies are the...
research
∙
08/22/2020
Learning the Boundary of Inductive Invariants
We study the complexity of invariant inference and its connections to ex...
research
∙
10/27/2019
Complexity and Information in Invariant Inference
This paper addresses the complexity of SAT-based invariant inference, a ...
research
∙
09/06/2019
Automating Cluster Management with Weave
Modern cluster management systems like Kubernetes and Openstack grapple ...
research
∙
05/19/2019
Inferring Inductive Invariants from Phase Structures
Infinite-state systems such as distributed protocols are challenging to ...
research
∙
02/25/2018
Secure Serverless Computing Using Dynamic Information Flow Control
The rise of serverless computing provides an opportunity to rethink clou...
research
∙
02/24/2018
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
We consider the problem of binary image generation with given properties...
research
∙
01/12/2018
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Callbacks are essential in many programming environments, but drasticall...
research
∙
10/24/2017
Bounded Quantifier Instantiation for Checking Inductive Invariants
We consider the problem of checking whether a proposed invariant Ï• expre...
research
∙
10/19/2017
Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Distributed protocols such as Paxos play an important role in many compu...
research
∙
09/19/2017
Verifying Properties of Binarized Deep Neural Networks
Understanding properties of deep neural networks is an important challen...
research
∙
08/19/2017
Abstractions for Verifying Isolation Properties in Stateful Networks
Modern networks achieve robustness and scalability by maintaining states...
research
∙
08/19/2017
