A study of the combination problem : dealing with multiple theories in SMT solving
Hoy en día, las aplicaciones de software son ubicuas en nuestras vidas, y sus fallas pueden, en muchos casos, producir enormes pérdidas. Esto hace esencial el desarrollo de métodos de análisis de software. Para esto, usualmente se asume que se cuenta con una especificación formal del sistema a anali...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Tesis de grado publishedVersion |
| Lenguaje: | Inglés |
| Publicado: |
Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
2014
|
| Materias: | |
| Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000702_Chocron https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000702_Chocron_oai |
| Aporte de: |
| Sumario: | Hoy en día, las aplicaciones de software son ubicuas en nuestras vidas, y sus fallas pueden, en muchos casos, producir enormes pérdidas. Esto hace esencial el desarrollo de métodos de análisis de software. Para esto, usualmente se asume que se cuenta con una especificación formal del sistema a analizar; entonces es posible verificar si cierta propiedad de interés se deduce de la especificación. La lógica es frecuentemente utilizada como sistema formal para la especificación y verificación, lo cual vuelve un problema crucial el decidir si una propiedad es satisfacible según determinadas teorías. Un problema de satisfacibilidad se expresa frecuentemente en una combinación de varias teorías, y un enfoque natural consiste en resolverlo combinando los procedimientos de decisión con los que se cuenta para cada una de las teorías. En esta tesis estudiamos el problema de combinación de procedimientos para teorías de primer orden sobre signaturas que comparten símbolos. Presentamos dos enfoques diferentes para resolver este problema. En el primero, extendemos el método de combinación clásico para teorías sobre signaturas disjuntas de Nelson y Oppen al caso en el cual sólo se comparten predicados unarios. Teorías relevantes se pueden analizar desde este marco, como por ejemplo la clase de teoría de Löwenheim. El segundo enfoque estudia un caso particular, en el cual el fragmento de signatura compartida resulta de definir funciones que conectan elementos de dos teorías sobre signaturas disjuntas. Un ejemplo clásico es el de las listas extendidas con una función de longitud que las relaciona con la aritmética. Presentamos un procedimiento para resolver este caso, y mostramos cómo se puede adaptarlo para considerar distintas clases de teorías y funciones. Este trabajo fue parcialmente desarrollado durante una pasantía en LORIA-INRIA, bajo la supervisión de Pascal Fontaine y Christophe Ringeissen, a quienes agradecemos especialmente. |
|---|