HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Combining Lists with Non-Stably Infinite Theories

Pascal Fontaine 1 Silvio Ranise 2 Calogero Zarba 2
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In program verification one has often to reason about lists over elements of a given nature. Thus, it becomes important to be able to combine the theory of lists with a generic theory $T$ modeling the elements. This combination can be achieved using the Nelson-Oppen method only if $T$ is stably infinite. The goal of this paper is to relax the stable-infiniteness requirement. More specifically, we provide a new method that is able to combine the theory of lists with any theory $T$ of the elements, regardless of whether $T$ is stably infinite or not. The crux of our combination method is to guess an arrangement over a set of variables that is larger than the one considered by Nelson and Oppen. Furthermore, our results entail that it is also possible to combine $T$ with the more general theory of lists with a length function.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Friday, October 21, 2005 - 6:00:04 PM
Last modification on : Friday, January 21, 2022 - 3:08:52 AM
Long-term archiving on: : Thursday, April 1, 2010 - 10:53:09 PM



Pascal Fontaine, Silvio Ranise, Calogero Zarba. Combining Lists with Non-Stably Infinite Theories. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), Mar 2005, Montevideo/Uruguay, pp.51--66, ⟨10.1007/b106931⟩. ⟨inria-00000481⟩



Record views


Files downloads