If you’d like to get in touch, direct your emails to: adamtaylor @ gmail . com. I am currently accepting new clients.
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, Q are fomulae in a base logic (e.g. full predicate logic etc.) and C is [...]
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 that States = Stacks x Heaps, so an assertion can refer to both stack and [...]
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 a branch of Computer Science responsible for formally proving the “correctness” of programmes. Usually, this [...]