Formal Methods

Formal methods Formal methods are techniques – usually based on mathematics – used for the specification, analysis and verification of software and hardware. Why would anyone be interested in formal methods? The main reasons to consider formal methods are verifying that a design is correct, verifying that a change is correct, analysing a system to learn about it and developing an intuition about the system. Formal methods is the umbrella term that contains several techniques inside of it We’ll be considering only model checking because I believe it is the easiest to get started with and get a return on the investment quickly. ...

This post contains TLA+ solutions for The Deadlock Empire which is a collection of challenges where the objective is to break multithreaded programs by playing the role of a scheduler that can context switch at any time. Non atomic instructions There’s two threads executing the following code: a = a + 1; if (a == 1) { critical_section(); } Since the a increment is not atomic, conceptually, it is like setting a temporary variable to the value of a– tmp = a and then setting a to the temporary variable value incremented by 1 – a = tmp + 1. ...