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.
Program Verification
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.
Why use formal specification
This blog explores the benefits of formal specification in the context of program verification.
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.