Search Results

Documents authored by Ihlemann, Carsten


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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail