We present a novel technique to combine satisfiability procedures for theories that model some data-structures and that share the integer offsets. This procedure extends the Nelson-Oppen approach to a family of non-disjoint theories that have practical interest in verification. The result is derived by showing that the considered theories satisfy the hypotheses of a general result on non-disjoint combination. In particular, the capability of computing logical consequences over the shared signature is ensured in a non trivial way by devising a suitable complete superposition calculus. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Nicolini, E., Ringeissen, C., & Rusinowitch, M. (2009). Satisfiability procedures for combination of theories sharing integer offsets. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5505 LNCS, pp. 428–442). https://doi.org/10.1007/978-3-642-00768-2_35
Mendeley helps you to discover research relevant for your work.