UPM / IMDEA Track in Software Development through Rigorous Methods

• Germán Puebla

4 credits (ECTS)

Good programming base. First order logic. Basic mathematics for computer science (functions, applications, set theory).

http://lml.ls.fi.upm.es/av/

There are powerful tools for the automatic and semi-automatic analysis, verification and processing of software. It is expected that in the short run these tools dramatically change the way software is developed. It is therefore very important to know how these tools work and have notions of the techniques that are based, in order to maximize their potential.

• Static analysis gives information about the behavior of programs without executing them. Abstract interpretation is an analysis framework which produces safe information which is valid for any program execution. There are many types of static analyses, some of which approximate not only the results of program, but also consumption of resources in terms of instructions executed, memory usage, etc.
• Verification can demonstrate the correctness of programs for any value of the input data. Therefore allows very powerful results, but not always is automatic.
• Finally, program transformation techniques make it possible to obtain program versions which are more efficient than the original program and to understand.

This course will study the main existing tools and techniques that allow underlying static analysis (in particular to approximate the consumption of resources), check is made and program transformation.

1. Static Analysis
   • Static Analysis vs. Dynamic Analysis
   • Static Analysis Tools
   • Fundamentals of Abstract Interpretation
   • Numerical Abstract Domains. Widening and narrowing.
2. Resource Consumption
   • Cost Models. Upper and lower bounds. Asymptotic cost
   • COSTA System
   • Brief Introduction to Java and Java byte code
   • Generating Recurrence Equations
3. Program Verification
   • First Order Logic and interactive demonstrations with the KeY System
   • JML specification language
   • Fundamentals of Logic Programs for Java
   • Translation of Logic Programs with JML
   • Interactive Verification Key Duties Test
4. Program Transformation
   • Folding and Unfolding Techniques
   • Partial Evaluation
   • Applications of Partial Evaluation

The grades will be determined by a process of continuous assessment using the average scores of the exercises to be proposed in the weekly lab.

These exercises will require using tools to be presented during the lectures course, as well as understanding the underlying analysis techniques, verification and program transformation.

• Nielson, Nielson, Hankin: "Principles of Program Analysis". 2nd Ed, 2005. Springer.
• E. Albert; P. Arenas; S. Genaim; G. Puebla and D. Zanardini: "Resource usage analysis and its application to resource certification". In Foundations of Security Analysis and Design V, FOSAD Tutorial Lectures, vol. 5705 of LNCS. Springer, 2009
• Bernhard Beckert; Reiner Hähnle; Peter H. Schmitt (Eds.): "Verification of Object-Oriented Software: The KeY Approach". 2006, Springer.
• N.D. Jones; C.K. Gomard and P. Sestoft: "Partial Evaluation and Automatic Program Generation". Prentice Hall International, June 1993.

Back to the initial page
Go to the IMDEA Software Institute page