8 papers
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…
Formal Methods in Robot Policy Learning and Verification: A Survey on Current Techniques and Future Directions
Anastasios Manganaris, Vittorio Giammarino, Ahmed H. Qureshi +1
As hardware and software systems have grown in complexity, formal methods have been indispensable tools for rigorously specifying acceptable behaviors, synthesizing programs to mee…
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…