Toward language-independent program verification

Ștefănescu, Andrei

Permalink

https://hdl.handle.net/2142/92779 Copy

Description

Title

Toward language-independent program verification

Author(s)

Ștefănescu, Andrei

Issue Date

2016-07-08

Director of Research (if dissertation) or Advisor (if thesis)

Roșu, Grigore

Doctoral Committee Chair(s)

Roșu, Grigore

Committee Member(s)

• Parthasarathy, Madhusudan
• Meseguer, José
• Gunter, Elsa
• Bjørner, Nikolaj

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Date of Ingest

2016-11-10T17:50:16Z

Keyword(s)

• program verification
• operational semantics
• automated reasoning
• logics
• 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.

Graduation Semester

2016-08

Type of Resource

text

Permalink

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

Copyright and License Information

Copyright 2016 Andrei Stefanescu

Owning Collections