Specifying Algorithms Using Non-Deterministic Computations

In this article, we will discuss the use of the formalism of non-deterministic computations as a language for specifying algorithms.

July 4, 2024

Deductive Verification as an Alternative to "Push-Button" Technologies

In this paper, the deductive verification approach is compared with other formal verification techniques, emphasizing the importance of correctness certificates in the verification process.

April 5, 2024

Verification-driven development

In this paper the ‘reasonable machine’ term is presented along with the hypothesis that all practically applicable computing paradigms can be represented in the form of such machines.

March 6, 2024

Program Verification: background and notation

This paper examines the field of program verification, emphasizing the precise implementation of algorithms through computational models like finite automata and Turing machines.

February 1, 2024