6 citations · 9 across the 6 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
cs.PL2017
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…
cs.PL2017★ 2 cited
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…
cs.LO2017
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…