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.
Papers
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.
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.
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.