Files in this item



application/pdfSTEFANESCU-DISSERTATION-2016.pdf (2MB)
(no description provided)PDF


Title:Toward language-independent program verification
Author(s):Ștefănescu, Andrei
Director of Research:Roșu, Grigore
Doctoral Committee Chair(s):Roșu, Grigore
Doctoral Committee Member(s):Parthasarathy, Madhusudan; Meseguer, José; Gunter, Elsa; Bjørner, Nikolaj
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):program verification
operational semantics
automated reasoning
programming languages
Abstract: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.
Issue Date:2016-07-08
Rights Information:Copyright 2016 Andrei Stefanescu
Date Available in IDEALS:2016-11-10
Date Deposited:2016-08

This item appears in the following Collection(s)

Item Statistics