15 citations · 32 across the 14 of their papers we have counts for
15 papers
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…
Bring Your Own Formats and Kernels: Composable Abstractions for Sparse Matrix Computation
Pratyush Das, Amirhossein Basareh, Artem Pelenitsyn +3
Real-world sparse matrices often feature multiple forms of structured sparsity -- rectangular dense blocks, diagonal bands, and scattered entries -- that no single storage format c…
KestRel: Relational Verification Using E-Graphs for Program Alignment
Robert Dickerson, Prasita Mukherjee, Benjamin Delaware
Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency.…
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…