ATAME is an automatic program specialization tool written in the Maude language that, given a set of assertions that model the desired behavior of a program, and a program that can violate any of these assertions, automatically generates a safe program in which all possible executions satisfy the assertions.
See in the summary section
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models