6 citations · 9 across the 6 of their papers we have counts for
6 papers
Parallel RAM from Cyclic Circuits
David Heath
Known simulations of random access machines (RAMs) or parallel RAMs (PRAMs) by Boolean circuits incur significant polynomial blowup, due to the need to repeatedly simulate accesses…
Symphony: Expressive Secure Multiparty Computation with Coordination
Ian Sweet, David Darais, David Heath +3
Context: Secure Multiparty Computation (MPC) refers to a family of cryptographic techniques where mutually untrusting parties may compute functions of their private inputs while re…
Relational Verification via Invariant-Guided Synchronization
Qi Zhou, David Heath, William Harris
Relational properties describe relationships that hold over multiple executions of one or more programs, such as functional equivalence. Conventional approaches for automatically v…
Proofs as Relational Invariants of Synthesized Execution Grammars
Caleb Voss, David Heath, William Harris
The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synt…
Completely Automated Equivalence Proofs
Qi Zhou, David Heath, William Harris
Verifying partial (i.e., termination-insensitive) equivalence of programs has significant practical applications in software development and education. Conventional equivalence ver…
Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Qi Zhou, David Heath, William Harris
Recursion-free Constrained Horn Clauses (CHCs) are logic-programming problems that can model safety properties of programs with bounded iteration and recursion. In addition, many C…