Tag Archives: verification

Floyd-Hoare Logic

Floyd-Hoare Logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programmes. The central feature is the Hoare triple. Hoare Triples A Hoare triple {P} C {Q} is a formula. P, … Continue reading

Posted in Software Engineering | Tagged | Comments Off

A Simple Assertion Language for Formal Verification

Following on from our introduction of the basic concepts required to start to understand formal verification, we shall define a simple assertion language. An assertion is a logic formula describing a set of states with some “interesting” property. Also, recall … Continue reading

Posted in Software Engineering | Tagged | Comments Off

Stacks, Heaps, Variables and Pointers

It is important to have a solid understanding of the difference between stacks and heaps, and variables and pointers, before one can embark on the task of learning about Formal Verification of C-like languages. What’s Formal Verification? Formal Verification is … Continue reading

Posted in Software Engineering | Tagged | Comments Off