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

Authors Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.5.9.18.pdf
  • Filesize: 1.17 MB
  • 20 pages

Document Identifiers

Author Details

Nikolaj S. Bjorner
Jasmin Christian Blanchette
Viorica Sofronie-Stokkermans
Christoph Weidenbach
and all authors of the abstracts in this report

Cite AsGet BibTex

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

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.
Keywords
  • Automated Deduction
  • Program Verification
  • Certification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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