DROPS

Document

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/DagRep.3.10.1

Deduction and Arithmetic (Dagstuhl Seminar 13411)

Authors: Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach

Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.

Cite as

Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach. Deduction and Arithmetic (Dagstuhl Seminar 13411). In Dagstuhl Reports, Volume 3, Issue 10, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.3.10.1,
  author =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  title =	{{Deduction and Arithmetic (Dagstuhl Seminar 13411)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias 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.3.10.1},
  URN =		{urn:nbn:de:0030-drops-44250},
  doi =		{10.4230/DagRep.3.10.1},
  annote =	{Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving}
}

Search Results

Documents authored by Weidenbach, Christoph

Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)

Abstract

Cite as

Deduction and Arithmetic (Dagstuhl Seminar 13411)

Abstract

Cite as

Thanks for your feedback!

Could not send message