Search Results

Documents authored by Sofronie-Stokkermans, Viorica

Document
DOI: 10.4230/DagRep.7.9.26
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Authors: Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17371 "Deduction Beyond First-Order Logic." Much research in the past two decades was dedicated to automating first-order logic with equality. However, applications often need reasoning beyond this logic. This includes genuinely higher-order reasoning, reasoning in theories that are not finitely axiomatisable in first-order logic (such as those including transitive closure operators or standard arithmetic on integers or reals), or reasoning by mathematical induction. Other practical problems need a mixture of first-order proof search and some more advanced reasoning (for instance, about higher-order formulas), or simply higher-level reasoning steps. The aim of the seminar was to bring together first-order automated reasoning experts and researchers working on deduction methods and tools that go beyond first-order logic. The seminar was dedicated to the exchange of ideas to facilitate the transition from first-order to more expressive settings.
Cite as

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli. Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). In Dagstuhl Reports, Volume 7, Issue 9, pp. 26-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{blanchette_et_al:DagRep.7.9.26,
  author =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  title =	{{Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)}},
  pages =	{26--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.9.26},
  URN =		{urn:nbn:de:0030-drops-85872},
  doi =		{10.4230/DagRep.7.9.26},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}
Document
DOI: 10.4230/DagRep.5.9.18
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)

Authors: Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach

Published in: Dagstuhl Reports, Volume 5, Issue 9 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15381 "Information from Deduction: Models and Proofs". The aim of the seminar was to bring together researchers working in deduction and applications that rely on models and proofs produced by deduction tools. Proofs and models serve two main purposes: (1) as an upcoming paradigm towards the next generation of automated deduction tools where search relies on (partial) proofs and models; (2) as the actual result of an automated deduction tool, which is increasingly integrated into application tools. Applications are rarely well served by a simple yes/no answer from a deduction tool. Many use models as certificates for satisfiability to extract feasible program executions; others use proof objects as certificates for unsatisfiability in the context of high-integrity systems development. Models and proofs even play an integral role within deductive tools as major methods for efficient proof search rely on refining a simultaneous search for a model or a proof. The topic is in a sense evergreen: models and proofs will always be an integral part of deduction. Nonetheless, the seminar was especially timely given recent activities in deduction and applications, and it enabled researchers from different subcommunities to communicate with each other towards exploiting synergies.
Cite as

Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach. Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). In Dagstuhl Reports, Volume 5, Issue 9, pp. 18-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.5.9.18,
  author =	{Bjorner, Nikolaj S. and Blanchette, Jasmin Christian and Sofronie-Stokkermans, Viorica and Weidenbach, Christoph},
  title =	{{Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)}},
  pages =	{18--37},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{9},
  editor =	{Bjorner, Nikolaj S. and Blanchette, Jasmin Christian and Sofronie-Stokkermans, Viorica and Weidenbach, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.9.18},
  URN =		{urn:nbn:de:0030-drops-56830},
  doi =		{10.4230/DagRep.5.9.18},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}
Document
DOI: 10.4230/DagSemProc.09411.3
Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms

Authors: Viorica Sofronie-Stokkermans

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
We study possibilities of reasoning about extensions of base theories with functions which satisfy certain recursion and homomorphism properties. Our focus is on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof. \begin{itemize} item[(1)] We show that the theory of absolutely free constructors is local, and locality is preserved also in the presence of selectors. These results are consistent with existing decision procedures for this theory (e.g. by Oppen). item[(2)] We show that, under certain assumptions, extensions of the theory of absolutely free constructors with functions satisfying a certain type of recursion axioms satisfy locality properties, and show that for functions with values in an ordered domain we can combine recursive definitions with boundedness axioms without sacrificing locality. We also address the problem of only considering models whose data part is the {em initial} term algebra of such theories. item[(3)] We analyze conditions which ensure that similar results can be obtained if we relax some assumptions about the absolute freeness of the underlying theory of data types, and illustrate the ideas on an example from cryptography. end{itemize} The locality results we establish allow us to reduce the task of reasoning about the class of recursive functions we consider to reasoning in the underlying theory of data structures (possibly combined with the theories associated with the co-domains of the recursive functions). As a by-product, the methods we use provide a possibility of presenting in a different light (and in a different form) locality phenomena studied in cryp-to-gra-phy; we believe that they will allow to better separate rewriting from proving, and thus to give simpler proofs.
Cite as

Viorica Sofronie-Stokkermans. Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{sofroniestokkermans:DagSemProc.09411.3,
  author =	{Sofronie-Stokkermans, Viorica},
  title =	{{Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--33},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.3},
  URN =		{urn:nbn:de:0030-drops-24241},
  doi =		{10.4230/DagSemProc.09411.3},
  annote =	{Keywords: Decision procedures, recursive datatypes, recursive functions, homomorphisms, verification, cryptography}
}
Document
DOI: 10.4230/DagSemProc.07401.6
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact