Showing 1–3 of 3 results for author: Berezun, D

Can LLMs Enable Verification in Mainstream Programming?

Authors: Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev

Abstract: Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini,… ▽ More Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results. △ Less

Submitted 18 March, 2025; originally announced March 2025.

Reimplementing the Wheel: Teaching Compilers with a Small Self-Contained One

Authors: Daniil Berezun, Dmitry Boulytchev

Abstract: We report on a one-semester compiler construction course based on the idea of implementing a small self-contained compiler for a small model language from scratch, not using other compiler construction frameworks. The course is built around an evolving family of languages with increasing expressiveness and complexity, which finally is crowned by a language with first-class functions, S-expressions… ▽ More We report on a one-semester compiler construction course based on the idea of implementing a small self-contained compiler for a small model language from scratch, not using other compiler construction frameworks. The course is built around an evolving family of languages with increasing expressiveness and complexity, which finally is crowned by a language with first-class functions, S-expressions, pattern matching, and garbage collection. The code generation technique is based on the idea of symbolic interpreters, which allows to implement a robust albeit not a very efficient native code generator. We give the motivation for the course, describe its structure, and report some results of teaching based on students' post-course surveys. △ Less

Submitted 26 July, 2022; originally announced July 2022.

Comments: In Proceedings TFPIE 2021/22, arXiv:2207.11600

Journal ref: EPTCS 363, 2022, pp. 22-43

An Empirical Study of Partial Deduction for miniKanren

Authors: Ekaterina Verbitskaia, Daniil Berezun, Dmitry Boulytchev

Abstract: We study conjunctive partial deduction, an advanced specialization technique aimed at improving the performance of logic programs, in the context of relational programming language miniKanren. We identify a number of issues, caused by miniKanren peculiarities, and describe a novel approach to specialization based on partial deduction and supercompilation. The results of the evaluation demonstrate… ▽ More We study conjunctive partial deduction, an advanced specialization technique aimed at improving the performance of logic programs, in the context of relational programming language miniKanren. We identify a number of issues, caused by miniKanren peculiarities, and describe a novel approach to specialization based on partial deduction and supercompilation. The results of the evaluation demonstrate successful specialization of relational interpreters. Although the project is at an early stage, we consider it as the first step towards an efficient optimization framework for miniKanren. △ Less

Submitted 6 September, 2021; originally announced September 2021.

Comments: In Proceedings VPT 2021, arXiv:2109.02001

Journal ref: EPTCS 341, 2021, pp. 73-94