A study of the combination problem : dealing with multiple theories in SMT solving

Mostrar todas las versiones(2)

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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Chocrón, Paula
Otros Autores: López Pombo, Carlos Gustavo
Formato: Tesis de grado publishedVersion
Lenguaje:Inglés
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2014
Materias:
SATISFACTIBILIDAD MODULO TEORIAS
ANALISIS DE SOFTWARE
MODULARIDAD
COMBINACION DE PROCEDIMIENTOS DE DECISION
SATISFIABILITY MODULO THEORIES
SOFWARE ANALYSIS
MODULARITY
COMBINATION OF DECISION PROCEDURES
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:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-seminario_nCOM000702_Chocron_oai
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Inglés
orig_language_str_mv eng
topic SATISFACTIBILIDAD MODULO TEORIAS
ANALISIS DE SOFTWARE
MODULARIDAD
COMBINACION DE PROCEDIMIENTOS DE DECISION
SATISFIABILITY MODULO THEORIES
SOFWARE ANALYSIS
MODULARITY
COMBINATION OF DECISION PROCEDURES
spellingShingle SATISFACTIBILIDAD MODULO TEORIAS
ANALISIS DE SOFTWARE
MODULARIDAD
COMBINACION DE PROCEDIMIENTOS DE DECISION
SATISFIABILITY MODULO THEORIES
SOFWARE ANALYSIS
MODULARITY
COMBINATION OF DECISION PROCEDURES
Chocrón, Paula
A study of the combination problem : dealing with multiple theories in SMT solving
topic_facet SATISFACTIBILIDAD MODULO TEORIAS
ANALISIS DE SOFTWARE
MODULARIDAD
COMBINACION DE PROCEDIMIENTOS DE DECISION
SATISFIABILITY MODULO THEORIES
SOFWARE ANALYSIS
MODULARITY
COMBINATION OF DECISION PROCEDURES
description 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.
author2 López Pombo, Carlos Gustavo
author_facet López Pombo, Carlos Gustavo
Chocrón, Paula
format Tesis de grado
Tesis de grado
publishedVersion
author Chocrón, Paula
author_sort Chocrón, Paula
title A study of the combination problem : dealing with multiple theories in SMT solving
title_short A study of the combination problem : dealing with multiple theories in SMT solving
title_full A study of the combination problem : dealing with multiple theories in SMT solving
title_fullStr A study of the combination problem : dealing with multiple theories in SMT solving
title_full_unstemmed A study of the combination problem : dealing with multiple theories in SMT solving
title_sort study of the combination problem : dealing with multiple theories in smt solving
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2014
url 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
work_keys_str_mv AT chocronpaula astudyofthecombinationproblemdealingwithmultipletheoriesinsmtsolving
AT chocronpaula unestudiodelproblemadecombinacionsolucionesasmtmodulovariasteorias
AT chocronpaula studyofthecombinationproblemdealingwithmultipletheoriesinsmtsolving
_version_ 1843126955082252288
spelling I28-R145-seminario_nCOM000702_Chocron_oai2025-08-20 López Pombo, Carlos Gustavo Chocrón, Paula 2014 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. Nowadays software artifacts are ubiquitous in our lives, and failures may, in many cases, produce enormous losses, making essential the development of methods to perform analysis over software. In order to do this, usually it is assumed that a formal specification of the system is available. Then, it is possible to check whether a certain property of interest follows from the specification. Logics have often been used as formal systems suitable for the specification and verification of software artifacts, making the problem of deciding if a property is satisfiable modulo some background theory crucial in verification. A satisfiability problem is very often expressed in a combination of theories, and a natural approach consists in solving the problem by combining the decision procedures available for the component theories. In this thesis, we study the problem of combining decision procedures for first-order theories over signatures sharing symbols. We present two different approaches. In the first one, we extend a classical combination method by Nelson and Oppen for theories over disjoint signatures to the case when only unary predicates are shared. Some well-known classes of theories fit in our framework, for example the Löwenheim class. The second approach focuses on a specific case, in which the non-disjointness arises from defining functions connecting terms in two theories with disjoint signatures. A classical example is the one of lists endowed with a length function that relates them with arithmetic. We present a procedure to solve this case, and discuss how it should be adapted to different classes of theories and functions. This work was partially developed during an internship at LORIA-INRIA, under the supervision of Pascal Fontaine and Christophe Ringeissen, to whom we thank specially. Fil: Chocrón, Paula. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000702_Chocron eng Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar SATISFACTIBILIDAD MODULO TEORIAS ANALISIS DE SOFTWARE MODULARIDAD COMBINACION DE PROCEDIMIENTOS DE DECISION SATISFIABILITY MODULO THEORIES SOFWARE ANALYSIS MODULARITY COMBINATION OF DECISION PROCEDURES A study of the combination problem : dealing with multiple theories in SMT solving Un estudio del problema de Combinación : soluciones a SMT módulo varias teorías info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000702_Chocron_oai

Ejemplares similares