5 papers · 1 filter
Polymorphic Coverage Types
Zhe Zhou, Ashish Mishra, Benjamin Delaware +1
Test input generators are an important part of property-based testing (PBT) frameworks, and a key expectation is that they be capable of producing all acceptable elements that sati…
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…
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…
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.…