Semantics-based program verification

Park, Daejun

Permalink

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

Description

Title

Semantics-based program verification

Author(s)

Park, Daejun

Issue Date

2019-04-09

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

Roşu, Grigore

Doctoral Committee Chair(s)

Roşu, Grigore

Committee Member(s)

• Adve, Vikram
• Miller, Andrew
• 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

Keyword(s)

• Program verification
• Program equivalence

Abstract

"We present language-independent formal methods that are parameterized by the operational semantics of languages. We provide the theory, implementation, and extensive evaluation of the language-parametric formal methods. Specifically, we consider two formal analyses: program verification and program equivalence. First, we propose a novel notion of bisimulation, which we call cut-bisimulation, allowing the two programs to semantically synchronize at relevant ""cut"" points, but to evolve independently otherwise. Employing the cut-bisimulation, we develop a language-independent equivalence checking algorithm, parameterized by the input and output language semantics, to prove equivalence of programs written in possibly different languages. We implement the algorithm in the K framework, yielding the first language-parametric program equivalence checker. To demonstrate the practical feasibility of the language-parametric formal methods, we instantiate a language-independent deductive program verifier by plugging-in four real-world language semantics, C, Java, JavaScript, and Ethereum Virtual Machine (EVM), and use them to verify full functional correctness of challenging heap-manipulating programs and high-profile commercial smart contracts. In particular, to the best of our knowledge, the JavaScript and EVM verifiers are the first deductive program verifier for these languages."

Graduation Semester

2019-05

Type of Resource

text

Permalink

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

Copyright and License Information

Copyright 2019 Daejun Park

Owning Collections