DROPS

Document

Local Theory Extensions, Hierarchical Reasoning and Applications to Verification

Authors: Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs

Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)

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.

Cite as

Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs. Local Theory Extensions, Hierarchical Reasoning and Applications to Verification. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@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/entities/document/10.4230/DagSemProc.07401.6},
  URN =		{urn:nbn:de:0030-drops-12507},
  doi =		{10.4230/DagSemProc.07401.6},
  annote =	{Keywords: Automated reasoning, Combinations of decision procedures, Verification}
}

Search Results

Documents authored by Ihlemann, Carsten

Local Theory Extensions, Hierarchical Reasoning and Applications to Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message