While abstract interpretation-based program verification is often performed offline, it can be very useful when it occurs interactively during software development, flagging errors as the program is written. However, while context- and path-sensitive global analysis over complex domains can provide the precision needed for effective verification and optimization, it can also be expensive when applied to large code bases, sometimes making interactive use impractical. On the other hand, in many program development situations modifications are small and isolated within a few components. The modular and incremental fixpoint algorithms used by the Ciao abstract interpretation framework take advantage of this to reuse as much as possible previous analysis results, reducing response times in interactive use. In this talk we will review these ideas and show how the integration of the Ciao framework within different IDEs takes advantage of these techniques to achieve effective verification on-the-fly, as the program is developed. We also demonstrate a number of embeddings of this framework within the browser, and show as an example an application for building interactive tutorials, which we have used for teaching abstract interpretation and verification.

Manuel Hermenegildo is Distinguished Professor at (and was the Founding Director of) the IMDEA Software Institute. He is also a full Prof. of Computer Science at the U. Politécnica de Madrid, UPM. Previously he held an Endowed Chair in Information Science and Technology at the U. of New Mexico. He was also project leader at the MCC research center and Adjunct Associate Prof. at the CS Department of the U. of Texas, both in Austin, Texas. See his home page for more information.

Research interests: Global Program Analysis, Verification, Debugging, and Optimization for Functional and Non-functional Properties (Time, Memory, Energy); Abstract Interpretation; Partial Evaluation; Parallelism and (Resource-Aware) Parallelizing Compilers; Constraint/Logic/Functional Programming Theory and Implementation; Abstract Machines; Computational Logic; Automatic Documentation Tools; Execution Visualization; Sequential and Parallel Computer Architecture.