Formalización de la aritmética de TLA+ en el asistente de pruebas Isabelle

TLA+ es un lenguaje para especificar sistemas distribuidos y concurrentes. Está basado en una lógica clásica de primer orden no-tipada y en una variante de la teoría de conjuntos estándar ZF, más una pequeña parte de lógica temporal. Una versión extendida del lenguaje, llamada TLA+2, permite además...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Vanzetto, Hernán P.
Otros Autores: Merz, Stephan
Formato: bachelorThesis trabajo final de grado publishedVersion
Lenguaje:Español
Publicado: Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario 2014
Materias:
verificación formal
asistente de pruebas
TLA+
axiomas
aritmética de números enteros
Acceso en línea:http://hdl.handle.net/2133/3561
http://hdl.handle.net/2133/3561
Aporte de:
Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR) de Universidad Nacional de Rosario

Ejemplares similares

Ejemplares similares