CiaoPP performs abstract-interpretation based, context-sensitive analysis and verification by transforming both high- and low-level program representations into Horn clauses and computing the semantics of such clauses. This semantics is computed over user-definable abstract domains, using fixpoint computation. In this talk, we will present recent results on the use of assertions to guide such fixpoint computations in multivariant abstract interpretations, in order to both improve precision and accelerate analysis. We will also present some results on analysis of parallelism and dealing with higher-order.

Manuel Hermenegildo is Distinguished Professor at (and was the Founding Director of) the IMDEA Software Institute. He is also full Prof. of Computer Science at the Tech. U. of 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: Energy-Aware Computing, Resource / non-functional property analysis, verification, and control; Global Program Analysis, Optimization, Verification, Debugging; Abstract Interpretation; Partial Evaluation; Parallelism and Parallelizing Compilers; Constraint/Logic/Functional Programming Theory and Implementation, Abstract Machines; Automatic Documentation Tools, Execution Visualization; Sequential and Parallel Computer Architecture.