Toward language-independent program verification

Recent years have seen a renewed interest in the area of deductive program verification, with focus on verifying real-world software components. Success stories include the verification of operating system kernels and of compilers. This dissertation describes techniques for automatically building efficient correct-by-construction program verifiers for real-world languages from operational semantics. In particular, reachability logic is proposed as a foundation for achieving language-independent program verification. Reachability logic can express both operational semantics and program correctness properties, and has a sound and (relatively) complete proof systems that derives the program correctness properties from the operational semantics. These techniques have been implemented in the K verification infrastructure, which in turn yielded automatic program verifiers for C, Java, and JavaScript. These verifiers are evaluated by checking the full functional correctness of challenging heap manipulation programs implementing the same data-structures in these languages (e.g. AVL trees). This dissertation also describes the natural proof methodology for automated reasoning about heap properties.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2016

Author dc:creator

• Ștefănescu, Andrei

Contributors dc:contributor

• Roșu, Grigore
• Parthasarathy, Madhusudan
• Meseguer, José
• Gunter, Elsa
• Bjørner, Nikolaj

• program verification
• operational semantics
• automated reasoning
• logics
• programming languages

Statement dc:rights

• Copyright 2016 Andrei Stefanescu

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/92779

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/92779