Files in this item



application/pdfPARK-DISSERTATION-2019.pdf (1MB)
(no description provided)PDF


Title:Semantics-based program verification
Author(s):Park, Daejun
Director of Research:Roşu, Grigore
Doctoral Committee Chair(s):Roşu, Grigore
Doctoral Committee Member(s):Adve, Vikram; Miller, Andrew; Bjørner, Nikolaj
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(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.
Issue Date:2019-04-09
Rights Information:Copyright 2019 Daejun Park
Date Available in IDEALS:2019-08-23
Date Deposited:2019-05

This item appears in the following Collection(s)

Item Statistics