• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Student
Title
Supervisor
Faculty
Educational Programme
Final Grade
Year of Graduation
Pavel Putro
Deductive Verification of Basic Blocks in Machine Code
Software Engineering
(Bachelor’s programme)
2018
When developing programs in high-level languages, developers have to make assumptions about the correctness of the compiler. However, this may be unacceptable for critical systems. As long as there are no full-fledged formally verified compilers, the author proposes to solve this problem by proving the correctness of the generated machine code by deductive verification. To achieve this goal, it is required to combine the pre- and postcondition specifications with the machine code behavior model. The paper presents an experimental study aiming to build an instrument that can prove machine code of C functions without loops using deductive verification and SMT-solvers. As a result, it can be used for proving real critical system written in C language and annotated by ACSL language.

The scientific novelty of the work consists in the using of the method of merging high-level language specifications with the machine code behavior model, developed by the author, as well as the use of the microprocessor architecture description language for the specification of the target processor model.

The paper contains 62 pages, 3 chapters 50 illustrations, 33 sources.

Index Terms— machine code, deductive verification, formal specification, ACSL, SMT-solvers, Frama-C, Why3.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses