License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5683/
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)
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 |
|
Collection: |
|
Dagstuhl Reports, Volume 5, Issue 9 |
|
Issue Date: |
|
2016 |
|
Date of publication: |
|
19.01.2016 |
