software

Link

Symbolic model-checkers

During the MSc Logic (see education page), I became interested in symbolic model-checking. This is a technique whereby one verifies that a certain fact, represented as a proposition in a formal language (such as a modal or temporal logic), is true on a given system represented by a mathematical model. Such methods are widely used in formal verification to ensure the correctness and reliability of complex systems, including software, hardware, and safety-critical applications.

Below are several symbolic model-checkers that I have written, both as term projects for courses and as part of my master's thesis.

Temporal constructive models

For information on the logic and models, see here.

Plausibility models

For information on the logic and models, see here.

Topological models