The correctness of software is critical in today's information society. We all know that small faults in technical systems can have catastrophic consequences. In this regard, model Checking is a well-known approach to check the safety of a program in a mathematical and algorithmic way. It is a fully automatic technique to decide whether a program is safe or not with respect to a given safety property. The set of well-known model checkers for software includes HiFrog[1] and UpProver[2] developed at Formal Verification and Security group at USI.
In a nutshell, HiFrog is a verifier of a single C program for several properties. UpProver is a verifier of several programs (somewhat close) based on one property. Both tools delegate the problem of checking safety to an external decision procedure (more concretely, an SMT solver) called OpenSMT [3]. In both tools there are several configurations for the user that can decide which suit their need: for instance level of precision, interpolation algorithm, assertion optimization, defining function summaries by user, etc
Considering HiFrog and UpProver as a backend written in C++, developing a frontend such that displays the workflow in a Web browser helps the users to get a better insight about the verification process. We propose the student develop a web interface for dynamic visualization of the workflow of HiFrog or UpProver while the code is running. Furthermore, the web interface should give the user the possibility to choose their desired configuration and understand better how the tool works.
To have an idea of how the verification tool works we enclose a simplified picture of Hifrog's architecture. HiFrog consists of two main components SMT encoder and interpolating SMT solver; and the function summaries. The components are initially configured with the theory and the interpolation algorithms. The tool then processes assertions sequentially using function summaries when possible. The results of a successful verification are stored as function summaries and failed verifications trigger a refinement phase or the printing of an error trace.
While this project does not require any theoretical background in Formal Methods, we will appreciate if the student already has some background knowledge in Logic and the Theory of Computation. Experience with frontend development (for e.g., HTML or JAVA) is required. The Assistant will provide the student to understand the workflow of the tools. Determining a suitable language/framework for dynamic visualization of C++ code is part of the student’s research work.
As a sample you may check the following web interfaces developed in other tools: https://formal.iti.kit.edu/projects/improve/reve/index.php https://rvt.iem.technion.ac.il/
