A formal prover for certain programs in the Javascript programming language

July 6, 2015 JavaScript Clojure formal proofs

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

Apple Keynote format (in Russian)

Buy Me a Coffee at ko-fi.com