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 5 modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both 5 and T are stably infinite. The goal of this paper 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 5 with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic. © Springer-Verlag Berlin Heidelberg 2005.

Combining data structures with nonstably infinite theories using many-sorted logic / Ranise, S.; Ringeissen, C.; Zarba, C. G.. - 3717:(2005), pp. 48-64. (Intervento presentato al convegno 5th International Workshop on Frontiers of Combining Systems, FroCoS 2005 tenutosi a Vienna, aut nel 2005) [10.1007/11559306_3].

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

Ranise S.;
2005-01-01

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 5 modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both 5 and T are stably infinite. The goal of this paper 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 5 with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic. © Springer-Verlag Berlin Heidelberg 2005.
2005
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-540-29051-3
978-3-540-31730-2
Ranise, S.; Ringeissen, C.; Zarba, C. G.
Combining data structures with nonstably infinite theories using many-sorted logic / Ranise, S.; Ringeissen, C.; Zarba, C. G.. - 3717:(2005), pp. 48-64. (Intervento presentato al convegno 5th International Workshop on Frontiers of Combining Systems, FroCoS 2005 tenutosi a Vienna, aut nel 2005) [10.1007/11559306_3].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333002
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 40
  • ???jsp.display-item.citation.isi??? ND
social impact