
MU-TERM
Demostrador
vrain
Demostrador
vrainMUTERM acepta diversos tipos de programas basados en el uso de reglas de reescritura y permite demostrar la terminación de los cómputos realizados por dichos programas. La herramienta funciona de modo completamente automático a dos niveles. Por un lado incluye un experto que aplica una serie de técnicas para la demostración de terminación empleando una estrategia predefinida para ello. En esta modalidad el usuario puede desentenderse completamente del modo en que la herramienta obtiene la demostración. Por otro lado, puede utilizarse para demostrar la terminación empleando técnicas específicas. En esta modalidad el usuario puede especificar diversos parámetros que permiten controlar la demostración; esto es de utilidad para especialistas y también es útil en la docencia de dichas técnicas. En cualquier caso, las diversas opciones pueden utilizarse sin intervención del usuario ya que se establecen configuraciones por defecto para su uso inmediato. En ambos casos, la herramienta produce informes detallados que enumeran las técnicas aplicadas para obtener la demostración. MUTERM ha participado con muy buenos resultados en diversas competiciones internacionales junto con herramientas de propósito similar.
Ver en el apartado del resumen
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models