Refining Refinement Types: Enhancing Type-Based Reasoning for Automated Verification and Testing

<p dir="ltr">Formal verification often requires making difficult tradeoffs between user effort and the strength of guarantees. Refinement type systems are an established formal reasoning technique that balance these competing objectives by leveraging automated theorem provers to verify semantically rich program properties automatically. While refinement types have been integrated into a number of mainstream programming languages, several practical and technical challenges stand in the way of wider adoption. In real-world scenarios, library specifications are frequently missing or incomplete, making it difficult to reason about clients of those libraries using refinement types. At the same time, existing refinement types struggle to capture the behavior of libraries with hidden internal state and cannot express properties beyond traditional functional correctness, including the completeness of test input generators. This dissertation addresses these challenges by extending refinement type systems to support more expressive specifications and more scalable type inference. Its specific contributions include integrating data-driven and symbolic reasoning techniques to abduce library specifications, developing novel type specifications that leverage advances in automata theory, and establishing new theoretical foundations for type-based reasoning about new categories of program behaviors. It also demonstrates the practical benefits of these theoretical advances on a variety of real-world software systems.</p>