VeriFly: On-the-fly Assertion Checking with CiaoPP∗ (tool presentation)

Fast response times are essential for the integration of global static analysis tools at early stages of the software development cycle. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In the CiaoPP static analysis and verification framework this challenge is addressed through incremental (contextand path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper we present how the integration of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text –the tool’s VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the-shelf “on-the-fly” syntax checking facilities (flycheck). Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process.