John Hatcliff, Robby, Patrice Chalin, and Jason Belt

Kansas State University, USA

Track: Technical Research
Session: Formal Analysis
Previous applications of symbolic execution (SymExe) have focused on bug-finding and test-case generation. However, SymExe has the potential to significantly improve usability and automation when applied to verification of software contracts in safety-critical systems. Due to the lack of support for processing software contracts and ad hoc approaches for introducing a variety of over/under-approximations and optimizations, most SymExe implementations cannot precisely characterize the verification status of contracts. Moreover, these tools do not provide explicit justifications for their conclusions, and thus they are not aligned with trends toward evidence-based verification and certification. We introduce the concept of "explicating symbolic execution" (xSymExe) that builds on a strong semantic foundation, supports full verification of rich software contracts, explicitly tracks where over/under-approximations are introduced or avoided, precisely characterizes the verification status of each contractual claim, and associates each claim with "explications" for its reported verification status. We report on case studies in the use of Bakar Kiasan, our open source xSymExe tool for SPARK Ada.