TAV-CPS/IoT 2018
Mon 16 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA 2018
Wed 18 Jul 2018 16:00 - 16:30 at Cairo - Session III Chair(s): Neville Grech

CiaoPP is a context-sensitive, abstract interpretation-based analyzer and verifier based on transforming both high- and low-level program representations into Horn clauses and inferring via fixpoint computation the abstract semantics of such clauses, over a set of user-definable abstract domains. In this talk I will review the CiaoPP approach, and present recent applications such as energy consumption verification, static analysis of the cost of run-time checks for assertions, and some recent results in combining incremental and modular analysis.

Slides of talk (ciaopp_dpa18.pdf)2.66MiB

Manuel Hermenegildo is a Full Professor and (Founding) Scientific Director of the IMDEA Software Institute. He is also a 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 Assoc. 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.

Wed 18 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Session IIIDPA at Cairo
Chair(s): Neville Grech University of Athens
16:00
30m
Talk
Horn Clause-based Program Analysis with CiaoPP
DPA
Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM)
File Attached
16:30
30m
Talk
QL + LGTM = Declarative Program Analysis for the Masses
DPA
File Attached