Combining data structures with nonstably infinite theories using many-sorted logic

Silvio Ranise 1 Christophe Ringeissen 1 Calogero Zarba 2
1 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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory modeling the data structure with a theory modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both theories are stably infinite. The goal of this report is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory with any theory of the elements, regardless of whether the latter is stably infinite or not. The results of this report generalize to many-sorted logic those recently obtained by Tinelli and Zarba for combining the so-called shiny theories with nonstably infinite theories in one-sorted logic.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00000570
Contributor : Christophe Ringeissen <>
Submitted on : Thursday, November 3, 2005 - 12:11:35 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

Citation

Silvio Ranise, Christophe Ringeissen, Calogero Zarba. Combining data structures with nonstably infinite theories using many-sorted logic. 5th International Workshop on Frontiers of Combining Systems - FroCoS'05, Sep 2005, Vienna/Austria, pp.48--64, ⟨10.1007/11559306⟩. ⟨inria-00000570⟩

Share

Metrics

Record views

240