License
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.5.9.18
URN: urn:nbn:de:0030-drops-56830
URL: http://drops.dagstuhl.de/opus/volltexte/2016/5683/
Go back to Dagstuhl Reports


Bjorner, Nikolaj S. ; Blanchette, Jasmin Christian ; Sofronie-Stokkermans, Viorica ; Weidenbach, Christoph
Weitere Beteiligte (Hrsg. etc.): Nikolaj S. Bjorner and Jasmin Christian Blanchette and Viorica Sofronie-Stokkermans and Christoph Weidenbach

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

pdf-format:
dagrep_v005_i009_p018_s15381.pdf (1 MB)


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.

BibTeX - Entry

@Article{bjorner_et_al:DR:2016:5683,
  author =	{Nikolaj S. Bjorner and Jasmin Christian Blanchette and Viorica Sofronie-Stokkermans and Christoph Weidenbach},
  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 =	{Nikolaj S. Bjorner and Jasmin Christian Blanchette and Viorica Sofronie-Stokkermans and Christoph Weidenbach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5683},
  URN =		{urn:nbn:de:0030-drops-56830},
  doi =		{10.4230/DagRep.5.9.18},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}

Keywords: Automated Deduction, Program Verification, Certification
Seminar: Dagstuhl Reports, Volume 5, Issue 9
Issue Date: 2016
Date of publication: 19.01.2016


DROPS-Home | Fulltext Search | Imprint Published by LZI