An SMT-based model checker for Petri nets focused on reachability problems that takes advantage of polyhedral reduction.
A tool to project Petri net reachability properties on reduced nets using polyhedral reduction.
A tool to accelerate the computation of the concurrency relation of a Petri net using polyhedral reduction.
A tool to automatically prove the correctness of polyhedral equivalences for Petri nets.
Formalization of separation logic using the Isabelle/HOL proof assistant, as well as the proof of formula rewriting results from a paper entitled “The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains”.
An educational project, targeting Master and PhD students to showcase the application of SMT methods in system verification, by developing a Petri net model checker for the reachability problem.