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…
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…
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…