Implementation of the STRategy-based Automatic Safety aSsurance tool (STRASS), an automatic program safety enforcement tool for the Maude programming language

Auditoría, Calidad y Fiabilidad (UCM, 2015)

Maude integration and verification for ROS Nav 2

Formal verification of Hybrid Post-Quantum TLS protocol

Exercises of Algorithms and Data Structures

The Open Deduction Proof Editor allows proof theorists (or anyone) to deconstruction proofs step by step. It currently supports deep inference formalisms, namely Open Deduction and naturally the Calculus of Structures. The front end of the application is written in Java, while the back end is written in Maude. There is also an implementation of …

Model checker for Maude systems controlled by strategies

Maude simulator for MultiVeSta

Narrowing with strategies in Maude

Specification-based Testing Concurrent Java Programs with JPF and Maude

Graphical interface and graph generator for the Maude strategy model checker

My blog; https://www.stevenmaude.co.uk

Maude language subset

Repo for assignments on NTIN043 (Formal Foundations of Software Engineering)

Language bindings for Maude

Pygments lexers for Maude, both batch and interactive.

This repository contains the Maude 2 interpreter source tree.

confluin does confluence checks for Tamarin input files

We have designed and implementd an algorithm to solve a unification problem modulo ACH (Associativity, Commutativity, Homomorphism) theory.

Basic Syntactic Mutation (BSM) is a mutation based unification algorithm for the theories that are saturated by paramodulation.