6 citations · 10 across the 5 of their papers we have counts for
5 papers · 1 filter
A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
Zhe Zhou, Qianchuan Ye, Benjamin Delaware +1
Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implem…
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
Qianchuan Ye, Benjamin Delaware
Secure multiparty computation (MPC) techniques enable multiple parties to compute joint functions over their private data without sharing that data with other parties, typically by…
HACCLE: Metaprogramming for Secure Multi-Party Computation -- Extended Version
Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik +17
Cryptographic techniques have the potential to enable distrusting parties to collaborate in fundamentally new ways, but their practical implementation poses numerous challenges. An…
RHLE: Modular Deductive Verification of Relational Properties
Robert Dickerson, Qianchuan Ye, Michael K. Zhang +1
Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about…
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit--Claudel +2
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more wor…