Registro:
| Documento: | Tesis de Grado |
| Título: | Recuperación de fórmulas culpables mediante análisis de unsat core |
| Autor: | Giménez, Francisco Andrés |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2025-06-12 |
| Fecha de defensa: | 2017 |
| Fecha en portada: | 2017 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Schapachnik, Fernando Pablo |
| Jurado: | Asteasuain, Fernando; Mera, Sergio Fernando |
| Idioma: | Español |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000644_Gimenez |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000644_Gimenez.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000644_Gimenez |
| Ubicación: | Dep.COM 000644 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Giménez, Francisco Andrés. (2017). Recuperación de fórmulas culpables mediante análisis de unsat core. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000644_Gimenez |
Resumen:
La verificación de modelos (en inglés model checking) es un método automático para verificar sistemas formales, escritos generalmente en algún tipo de lógica temporal. A lo largo de los años se fueron creando nuevas técnicas dentro de esta área para poder realizar la tarea más eficientemente. Una de ellas es conocida como Bounded Model Checking (BMC), que en general se trata de utilizar internamente procesos SAT para realizar la verificación deseada sobre un determinado modelo. FormaLex es una herramienta desarrollada para verificar coherencia de documentos normativos escritos en un lenguaje basado en lógica temporal. Internamente utiliza un model checker para poder constatar dicha coherencia. Sin embargo, existen casos en los que la información que estos brindan no es suficiente para determinar de manera certera que no existan incoherencias entre las normas legales analizadas. Este trabajo explora el uso del núcleo de insatisfacibilidad (unsat core) para refinar el análisis de FormaLex. Se documenta una modificación que se puede realizar dentro del model checker NuSMV (invocado por FormaLex para validar el modelo generado), en conjunto con el SAT solver Picosat, para que se pueda analizar el unsat core de la fórmula booleana generada al realizar BMC, contribuyendo así a detectar contradicciones entre fórmulas normativas.
Citación:
---------- APA ----------
Giménez, Francisco Andrés. (2017). Recuperación de fórmulas culpables mediante análisis de unsat core. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000644_Gimenez
---------- CHICAGO ----------
Giménez, Francisco Andrés. "Recuperación de fórmulas culpables mediante análisis de unsat core". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2017.https://hdl.handle.net/20.500.12110/seminario_nCOM000644_Gimenez
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000644_Gimenez.pdf
Distrubución geográfica
