Abstracts

This thesis introduces the foundation of an API for building constraint solving problems for the Korat solver for imperative predicates. Our goal is two-fold: (1) to facilitate the use of Korat as a backend solver for applications that desire using it as a constraint solving engine; and (2) to facilitate optimized analyses using Korat, which follow the spirit of modern constraint solving and software testing techniques. We describe the API and how it uses the core Korat engine, and demonstrate the benefits in two application contexts: (1) using Korat as a backend engine for model counting; and (2) using Korat as test generator. We believe our work introduces a promising approach for making the ability of Korat to efficiently solve imperative predicates more widely applicable, possibly even in new application contexts where Korat has net been used before.Advisors/Committee Members: Khurshid, Sarfraz (advisor), Zhang, Lingming (committee member).