nicolasAmat
Postdoctoral researcher at IMDEA Software Institute | Participant in the Model Checking Contest
IMDEA Software InstituteMadrid, Spain
Pinned Repositories
Kong
Kong is a tool to compute the concurrency relation of a Petri using nets reduction (polyhedral approach).
matrix2pnml
MCC-Reachability
Oracles from the MCC 2022 for the Reachability category
Octant
Quantifier eliminator for using Petri net reductions for model checking reachability properties.
Reductron
Reductron - The Polyhedral Abstraction Prover
Separation-Logic-Formalization
Formalisation of the Separation Logic on Isabelle
SMPT
SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).
Sudoku_Solver
A Sudoku solver with a custom DPLL decision procedure.
tipx
uSMPT
µSMPT: An environnement to experiment with SMT-based model checking for Petri nets
nicolasAmat's Repositories
nicolasAmat/SMPT
SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).
nicolasAmat/Kong
Kong is a tool to compute the concurrency relation of a Petri using nets reduction (polyhedral approach).
nicolasAmat/MCC-Reachability
Oracles from the MCC 2022 for the Reachability category
nicolasAmat/uSMPT
µSMPT: An environnement to experiment with SMT-based model checking for Petri nets
nicolasAmat/Octant
Quantifier eliminator for using Petri net reductions for model checking reachability properties.
nicolasAmat/Reductron
Reductron - The Polyhedral Abstraction Prover
nicolasAmat/Sudoku_Solver
A Sudoku solver with a custom DPLL decision procedure.
nicolasAmat/tipx
nicolasAmat/matrix2pnml
nicolasAmat/pnets
A set of tools written in rust to manipulate petri nets.
nicolasAmat/ReachPT_CP_Benchmark_Suite
Collection of reachability formulas on Petri nets written in the MiniZinc language.
nicolasAmat/Separation-Logic-Formalization
Formalisation of the Separation Logic on Isabelle
nicolasAmat/benchmark-submission
Git repository for the submission of SMT-LIB benchmarks
nicolasAmat/Artifact-Octant
Artifact for Paper "Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability"
nicolasAmat/Concrete-Semantics
Learning Isabelle with Concrete Semantics book.
nicolasAmat/dotfiles
My Archlinux - i3wm - zsh - neovim setup
nicolasAmat/drawio
nicolasAmat/E-Abstraction
Formalization of the E-Abstraction Equivalence using Isabelle/HOL
nicolasAmat/FV-NFLlib
Library implementing the Fan-Vercauteren homomorphic encryption scheme
nicolasAmat/mcc
High-Level Nets Blaster for the Model-Checking Contest
nicolasAmat/MCF
nicolasAmat/NFLlib
NTT-based Fast Lattice library
nicolasAmat/nicolasAmat
Config files for my GitHub profile.
nicolasAmat/nicolasAmat.github.io
nicolasAmat/pnmcc-models-2020
Models, Formulas, Oracles from Model Checking Competition 2020
nicolasAmat/the-omega-project
Tools from Pugh et al.'s "Omega Project" for constraint-based compiler tools: The "Omega Library" for constraint manipulation; The "Omega Calculator" (text interface); the "Omega Test" for depedence analysis; the "Uniform Library" for code transformation; and the "Code generation" library for generating the transformed code. I am experimenting with tracking bugs with Lighthouse, but am not yet sure I've got it configure right --- see http://davew_haverford.lighthouseapp.com/projects/13658-the-omega-project/overview (if you can; if you can't, email davew@cs.haverford.edu).
nicolasAmat/XPIR
XPIR: Private Information Retrieval for Everyone