15 citations · 24 across the 11 of their papers we have counts for
7 papers · 1 filter
Trace-Guided Synthesis of Effectful Test Generators
Zhe Zhou, Ankush Desai, Benjamin Delaware +1
Several recently proposed program logics have incorporated notions of underapproximation into their design, enabling them to reason about reachability rather than safety. In this p…
From Traces to Program Incorrectness: A Type-Theoretic Approach
Yongwei Yuan, Zhe Zhou, Julia Belyakova +2
We present a type-theoretic framework for reasoning about incorrectness in functional programs that interact with effectful, opaque library APIs. Our approach centers on traces --…
Type-Based Incorrectness Reasoning
Zhe Zhou, Benjamin Delaware, Suresh Jagannathan
A coverage type generalizes refinement types found in many functional languages with support for must-style underapproximate reasoning. Property-based testing frameworks are one pa…
We've Got You Covered: Type-Guided Repair of Incomplete Input Generators
Patrick LaFontaine, Zhe Zhou, Ashish Mishra +2
Property-based testing (PBT) is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of thi…
Derivative-Guided Symbolic Execution
Yongwei Yuan, Zhe Zhou, Julia Belyakova +1
We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of li…
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…
Data-Driven Abductive Inference of Library Specifications
Zhe Zhou, Robert Dickerson, Benjamin Delaware +1
Programmers often leverage data structure libraries that provide useful and reusable abstractions. Modular verification of programs that make use of these libraries naturally rely…