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
Repository : https://gitlab.com/dqalvarez/thacheck
Language : Python ^3.12
Logic : Temporal intuitionistic logic
Models : Temporal Heyting algebras
For information on the logic and models, see here.
Plausibility models
Repository : https://gitlab.com/dqalvarez/smcplaus
Language : Python ^3.11
Logic : Plausibility logic
Models : Plausibility models
For information on the logic and models, see here.
Topological models
Repository : https://gitlab.com/dqalvarez/topomodels
Language : Haskell
Logic : Modal logic
Models : Topological spaces