UAIC - Grant Intern


Continut

(this page is mostly in Romanian - special request of the funding institution)


Informatii generale


Descriere

Verificarea programelor este o problema la fel de veche precum informatica în sine, deoarece primele rezultate în acest domeniu au apărut în anii '60. Această problemă este importantă deoarece multe sisteme critice (de exemplu: sisteme medicale, energie, transport) depind de corectitudinea programelor pentru a ne asigura că ele funcționează corect. În același timp, această problemă este dificilă: ea este nedecidabilă în general, încă intractabilă în practică, lăsând mult loc pentru progres în această direcție.

Recent, în domeniul semanticilor (formale) operaționale ale limbajelor de programare, care pentru o perioadă lungă de timp au fost studiate doar teoretic și pe limbaje foarte mici, s-a făcut un progres semnificativ spre limbaje de programare obișnuite.

Concomitent cu descoperirile în domeniul semanticilor operaționale, printre altele, a fost propusă și o abordare practică pentru verificarea de programe, bazată pe execuție simbolică, căreia i-a fost demonstrată corectitudinea în Coq. Această abordare constă într-o procedură pentru verificare care este parametrică în semantica operațională (formală) a unui limbaj de programare. Dată o astfel de semantică și o specificație pentru un program, procedura încearcă să demonstreze specificația utilizând execuția simbolică.

Codificarea procedurii în Coq deschide calea combinării dintre verificarea automată și cea interactivă de programe într-un cadru independent de limbajul de programare.

Acest proiect își propune să utilizeze codificarea procedurii de verificare din Coq. Mai precis, vrem să demonstrăm că abordarea este fezabilă în practică și să arătăm că instrumentul curent poate fi utilizat pe mai multe programe relevante din mai multe limbaje de programare. Scopul final este obținerea de certificate pentru corectitudinea programelor.


Description (english)

Program verification is an old problem as far as computer science goes, since the first results date from the '60s. It is an important problem, since many critical safety-systems (e.g., in health care, energy, and transportation) depend on the correctness of programs in order to function properly. It is also a difficult problem: undecidable in general, still mostly untractable in practice, it leaves much room for progress.

Recently, the field of formal operational semantics of programming languages, which for a long time had been confined to theoretical studies on toy languages, has made significant progress towards real-life programming languages.

At the same pace with the recent discoveries in formal operational semantics, among the others, a more practically-oriented approach for program verification, based on the language-independent symbolic execution has been proved to be sound in Coq. This approach consists of a procedure for verification which is parametric in the (formal) operational semantics of a programming language. Given a language semantics and some program specifications, the procedure attempts to prove the latter using symbolic execution.

The embedding of the procedure in Coq opens the way to combining interactive and automatic program verification in a language-independent setting.

The proposed research topic is meant to use the embedding of the procedure for verification in Coq. Specifically, we wish to demonstrate that the approach is feasible in practice and usable on relevant examples from several languages from different programming paradigms. The final goal is to obtain certificates of correctness for programs.