News Archives

[Colloquium] Resource Usage Analysis and Verification in the CiaoPP System

August 25, 2011

Watch Colloquium: 

M4V file (688 MB)


  • Date: Thursday, August 25, 2011 
  • Time: 11:00 am — 11:50 am 
  • Place: Centennial Engineering Center Stamm Room (next to the southeast entrance)

Pedro Lopez-Garcia, PhD,
Researcher, IMDEA Software Institute, Madrid, Spain

We present a general resource usage analysis framework which is parametric with respect to resources and type of approximation (lower- and upper-bounds). The user can define the parameters of the analysis for a particular resource by means of assertions that associate basic cost functions with elementary operations of programs, thus expressing how they affect the usage of a particular resource. A global static analysis can then infer bounds on the resource usage of all the procedures in the program, providing such usage bounds as functions of input data sizes. We show how to instantiate such a framework for execution time analysis. Other examples of resources that can be analyzed by instantiating the framework are execution steps, energy consumption, as well as other user-defined resources, like the number of bits sent or received by an application over a socket, number of calls to a procedure, or number of accesses to a database. Based on the general analysis, we also present a framework for (static) verification of general resource usage program properties. The framework extends the criteria of correctness as the conformance of a program to a specification expressing upper and/or lower bounds on resource usages (given as functions on input data sizes). We have defined an abstract semantics for resource usage properties and operations to compare the (approximated) intended semantics of a program (i.e., the specification) with approximated semantics inferred by static analysis. These operations include the comparison of arithmetic functions. A novel aspect of our framework is that the outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. We have implemented these techniques within the Ciao/CiaoPP system in a natural way, resulting in a framework that unifies static verification and static debugging (as well as run-time verification and unit testing).

 

Bio: Pedro Lopez-Garcia, PhD, received a MS degree and a Ph.D. in Computer Science from the Technical University of Madrid (UPM), Spain in 1994 and 2000, respectively. In May 28, 2008 he got a Scientific Researcher position at the Spanish Council for Scientific Research (CSIC) and joined the IMDEA Software Institute. Immediately prior to this position, he held associate and assistant professor positions at UPM and was deputy director of the Artificial Intelligence unit at the Computer Science Department. He has published about 30 refereed scientific papers (50% of them at conferences and journals of high or very high impact.) He has also been coordinator of the international project ES_PASS and participated as a researcher in many other national and international projects. His main areas of interest include automatic analysis and verification of global and complex program properties such as resource usage (user defined, execution time, memory, etc.), non-failure and determinism; performance debugging; (automatic) granularity analysis/control for parallel and distributed computing; profiling; unit-testing; type systems; constraint and logic programming.