License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.07401.6
URN: urn:nbn:de:0030-drops-12507
URL: http://dagstuhl.sunsite.rwth-aachen.de/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:
07401.SofronieStokkermansViorica.Paper.1250.pdf (0.2 MB)

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:DagSemProc.07401.6,
  author =	{Sofronie-Stokkermans, Viorica and Ihlemann, Carsten and Jacobs, Swen},
  title =	{{Local Theory Extensions, Hierarchical Reasoning and Applications to Verification}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2007/1250},
  URN =		{urn:nbn:de:0030-drops-12507},
  doi =		{10.4230/DagSemProc.07401.6},
  annote =	{Keywords: Automated reasoning, Combinations of decision procedures, Verification}
}

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI