License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-12507
URL: http://drops.dagstuhl.de/opus/volltexte/2007/1250/
Go to the corresponding Portal


Sofronie-Stokkermans, Viorica ; Ihlemann, Carsten ; Jacobs, Swen

Local Theory Extensions, Hierarchical Reasoning and Applications to Verification

pdf-format:
Document 1.pdf (254 KB)


Abstract

Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions of literals in a background theory. This can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We present some new results on hierarchical and modular reasoning in complex theories, as well as several examples of application domains in which efficient reasoning is possible. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of local theory extension.

BibTeX - Entry

@InProceedings{sofroniestokkermans_et_al:DSP:2007:1250,
  author =	{Viorica Sofronie-Stokkermans and Carsten Ihlemann and Swen Jacobs},
  title =	{Local Theory Extensions, Hierarchical Reasoning and Applications to Verification},
  booktitle =	{Deduction and Decision Procedures},
  year =	{2007},
  editor =	{Franz Baader and Byron Cook and J{\"u}rgen Giesl and Robert Nieuwenhuis},
  number =	{07401},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2007/1250},
  annote =	{Keywords: Automated reasoning, Combinations of decision procedures, Verification}
}

Keywords: Automated reasoning, Combinations of decision procedures, Verification
Seminar: 07401 - Deduction and Decision Procedures
Issue Date: 2007
Date of publication: 29.11.2007


DROPS-Home | Fulltext Search | Imprint Published by LZI