6 citations · 10 across the 9 of their papers we have counts for
8 papers · 1 filter
Liquid Tree Automata
Ashish Mishra, Suresh Jagannathan
Component-based synthesis (CBS) generates loop-free programs from library components to satisfy logical queries. While expressive specifications and precise queries simplify the so…
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…
Close is Good Enough: Component-Based Synthesis Modulo Logical Similarity
Ashish Mishra, Suresh Jagannathan
Component-based synthesis (CBS) aims to generate loop-free programs from a set of libraries whose methods are annotated with specifications and whose output must satisfy a set of l…
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…