Analiza programelor - curs

Prezentare

Marţi, orele 18-20, sala A109 (Fac. de Automatică şi Calculatoare), din 27 aprilie 2004, timp de 6 săptămâni
Cadru didactic: Marius Minea, marius@cs.upt.ro>

Cursul e adresat tuturor celor interesaţi de programare, limbaje, instrumente de dezvoltare şi analiză, tehnici utilizate, rezultate noi, şi perspectiva de a lucra în domeniu: proiecte de diplomă, şi de cercetare.

Motivaţie

Sistemele software sunt tot mai complexe. Trebuie să detectăm erori sau probleme de securitate, sau şi mai greu, să garantăm absenţa lor; să analizăm funcţionarea şi performanţa programelor; sau chiar să definim un nou limbaj şi să implementăm un mediu de dezvoltare. Deci, trebuie să ştim ce tehnici şi instrumente există, şi cum să realizăm altele la nevoie.

Rezultatele de cercetare recente în domeniul analizei programelor sunt spectaculoase:

s-a verificat absenţa erorilor la rulare (ex. depăşiri) în programul de control din Airbus A340
s-au detectat automat şi corectat sute de erori în surse de sistem de operare (nucleul Linux)
s-a verificat corectitudinea secvenţelor de apeluri sistem în cod de > 100 k linii sursă (gcc)

Conţinut

Domeniul analizei programelor grupează o serie de tehnici pentru a deduce proprietăţi ale programelor prin analiza codului sursă, fără a rula executabilul. Vom discuta patru abordări: analiza fluxului de date, analiza bazată pe constrângeri, interpretare abstractă, sisteme de tipuri, prezentând succint principiile şi aplicabilitatea lor în practică: calculul fluxului de valori din program (pentru detectarea de atribuiri eronate), analiza atribuirilor indirecte prin pointeri, analiza structurilor alocate dinamic, simplificarea programelor la proprietăţile relevante pentru analiza dorită, instrumentarea cu verificări la rulare sau înlocuirea lor cu verificări statice.

Cerinţe

Noţiuni fundamentale de limbaje de programare, gândire algoritmică şi matematică. Cursul e înrudit cu cele de limbaje şi compilatoare, dar se poate urma independent.
Nu vor fi note sau teme, ci doar o serie de expuneri ca prim pas spre un curs opţional, dacă există interes.

Note de curs

Introducere. Analiza fluxului de date. PDF, 1:1 şi 1:6, pentru listat
Analiza fluxului de date. Sistematizare. PDF, 1:1 şi 1:6, pentru listat (versiune incompletă)
Interpretare abstractă PDF, 1:1 şi 1:6, pentru listat
Folii cu exemple de widening/narrowing (Doug Gregor, RPI)
Analiza bazata pe constrângeri
Un articol de sinteză de Alex Aiken
Sisteme de tipuri
Foliile din cursul lui Zhendong Su (UC Davis)
Luca Cardelli. Type Systems
Aplicatii: Splint, ESC/Java, CIL, CCured ...

Cursuri la alte universităţi

Program Analysis, Hanne Riis Nielson, Danmarks Tekniske Universitet (cu folii de curs după cartea autorului.
Graduate Seminar on Program Analysis, Zhendong Su, University of California at Davis
Program Analysis and Understanding, University of Maryland

Articole (lectură suplimentară)

Interpretare abstractă
Patrick Cousot. Abstract Interpretation Based Formal Methods and Future Challenges.. O descriere generală a problematicii interpretării abstracte şi o comparaţie cu alte metode de analiză.
Analizorul static ASTRÉE folosit pentru programul de control din Airbus A340

Marius Minea

Last modified: Tue May 25 14:45:21 EEST 2004