FSU Computer Science Assistant Professor, Dr. Grigory Fedyukovich, has received the Amazon Research Award for his project “Applying FreqHorn to verification of AWS C Common programs”.
A recent trend in automated software verification is to delegate the computational tasks to solvers for Satisfiability Modulo Theories (SMT) and Constrained Horn Clauses (CHC). The latter allows synthesizing inductive invariants and enables sound (but possibly incomplete) reasoning about loopy programs. Existing approaches to solving CHC are limited mainly to lightweight and imprecise first-order theories or expensive and impractical bit-precise reasoning. Supporting arrays and algebraic data types (ADT) is challenging due to the presence of quantifiers, but it is needed for a range of real-world applications such as Code-Level Model Checking in the Software Development Workflow by Amazon Web Services (called AWS C Common library). This proposal aims to extend a successful technique for CHC solving, implemented in a tool called FreqHorn and maintained at FSU. We will focus on the development of an automated converter from the AWS verification language to CHC, and we will exploit various different modeling paradigms that could serve to improve the scalability of verification.
The award includes funding in the amount of $60,000 for one year.