2026-09-20T02:15:37Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/104795 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Roşu, Grigore Roşu, Grigore Adve, Vikram Miller, Andrew Bjørner, Nikolaj Park, Daejun 2019-08-23T19:51:44Z 2019-08-23T19:51:44Z 2019-04-09 2019-05 "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." Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms The student, Daejun Park, accepted the attached license on 2019-04-08 at 23:27. The student, Daejun Park, submitted this Dissertation for approval on 2019-04-08 at 23:32. This Dissertation was approved for publication on 2019-04-09 at 09:29. DSpace SAF Submission Ingestion Package generated from Vireo submission #13528 on 2019-08-22 at 14:42:21 Made available in DSpace on 2019-08-23T19:51:44Z (GMT). No. of bitstreams: 2 PARK-DISSERTATION-2019.pdf: 1191120 bytes, checksum: 7af3f4a7c8d39554c05f9452fb11a000 (MD5) LICENSE.txt: 4208 bytes, checksum: 66de8493a06d73172fa93f89c996c92b (MD5) Previous issue date: 2019-04-09 application/pdf http://hdl.handle.net/2142/104795 en Copyright 2019 Daejun Park Program verification Program equivalence Semantics-based program verification text text Computer Science Computer Science University of Illinois at Urbana-Champaign Dissertation Ph.D.