Semantics-based program verification

"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."

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

2019

Author dc:creator

• Park, Daejun

Contributors dc:contributor

• Roşu, Grigore
• Adve, Vikram
• Miller, Andrew
• Bjørner, Nikolaj

• Program verification
• Program equivalence

Statement dc:rights

• Copyright 2019 Daejun Park

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

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