A formal prover for certain programs in the Javascript programming language
This thesis is concerned with developing an automatic system for sound formal proofs of programs written in a certain imperative subset of Javascript with logical annotations.
A graduate thesis by Leonid Shevtsov, completed at the Dnipropetrovsk National University’s Computer Technology chair, under the supervision of Alexander Khizha
Abstract
This thesis is concerned with developing an automatic system for sound formal proofs of programs written in a certain imperative subset of Javascript with logical annotations.
Source code
The source code and instructions can be obtained at the project’s page on GitHub.
Text
Supplementary text of the thesis (in Ukrainian, PDF format)
Presentation