Recent Publications

. Type-Guided Worst-Case Input Generation. In POPL, 2019.


. A Denotational Semantics for Nondeterminism in Probabilistic Programs. Working paper, 2018.


. Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization. In ESOP, 2017.

PDF Artifact

Recent Posts

Suppose you have a toy specification with built-in nondeterminism, and you want to generate answers with respect to the specification: type exp = EInt of int | EPair of exp * exp | ENdet of exp * exp type ans = VInt of int | VPair of ans * ans For example, from the following specification EPair (ENdet (EInt 5) (EInt 6)) (ENdet (EInt 7) (EInt 8)) you might want to generate a bunch of possible answers: