Heurísticas de búsqueda de prueba automática en la herramienta de análisis invariante de maude

La herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de los sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta la heurística de búsqueda automática de pruebas en el núcleo de la herramienta Maude Invariant Analyzer Tool, que proporciona un grado sustancial de automatización y puede descargar automáticamente muchas obligaciones de prueba sin la intervención del usuario. Estas heurísticas pueden aprovechar los predicados de igualdad definidos por ecuaciones e incluir técnicas de reescritura, reducción y búsqueda de pruebas basadas en SMT.

• Autores: Rocha, Camilo
• Tipo de recurso: Trabajo de grado de pregrado
• Fecha de publicación: 2013
• Institución: Universidad Autónoma de Bucaramanga - UNAB
• Repositorio: Repositorio UNAB
• Idioma: spa
• OAI Identifier: oai:repository.unab.edu.co:20.500.12749/8909
• Acceso en línea: http://hdl.handle.net/20.500.12749/8909
• Palabra clave: Innovaciones tecnológicas; Ciencia de los computadores; Desarrollo de tecnología; Ingeniería de sistemas; Investigaciones; Tecnologías de la información y las comunicaciones; TIC´s; Technological innovations; Computer science; Technology development; Systems engineering; Investigations; Information and communication technologies; ICT's; Proof-search heuristics; Rewriting logic; Innovaciones tecnológicas; Ciencias de la computación; Desarrollo tecnológico; Ingeniería de sistemas; Heurística de búsqueda de pruebas; Reescritura de lógica
• License: Derechos de autor 2013 Revista Colombiana de Computación