Local Theory Extensions, Hierarchical Reasoning and Applications to Verification

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

doi:10.4230/DagSemProc.07401.6

Document

Local Theory Extensions, Hierarchical Reasoning and Applications to Verification

Authors Viorica Sofronie-Stokkermans, Carsten Ihlemann, Swen Jacobs

Part of: Volume: Dagstuhl Seminar Proceedings, Volume 7401
Part of: Series: Dagstuhl Seminar Proceedings (DagSemProc)
License: Creative Commons Attribution 4.0 International license
Publication Date: 2007-11-29

PDF

File

PDF

DagSemProc.07401.6.pdf

Filesize: 254 kB
22 pages

Document Identifiers

DOI: 10.4230/DagSemProc.07401.6
URN: urn:nbn:de:0030-drops-12507

Subject Classification

Keywords

Automated reasoning
Combinations of decision procedures
Verification

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/DagSemProc.07401.6

Author Details

Viorica Sofronie-Stokkermans

Carsten Ihlemann

Swen Jacobs

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail