3 Search Results for "Reger, Giles"


Document
Principles of Contract Languages (Dagstuhl Seminar 22451)

Authors: Dilian Gurov, Reiner Hähnle, Marieke Huisman, Giles Reger, and Christian Lidström

Published in: Dagstuhl Reports, Volume 12, Issue 11 (2023)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22451 "Principles of Contract Languages". At the seminar, participants discussed the fundamental aspects of software contracts. Topics included the format and expressiveness of contracts, their use cases in software development and analysis, and contract composition and decomposition.

Cite as

Dilian Gurov, Reiner Hähnle, Marieke Huisman, Giles Reger, and Christian Lidström. Principles of Contract Languages (Dagstuhl Seminar 22451). In Dagstuhl Reports, Volume 12, Issue 11, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Article{gurov_et_al:DagRep.12.11.1,
  author =	{Gurov, Dilian and H\"{a}hnle, Reiner and Huisman, Marieke and Reger, Giles and Lidstr\"{o}m, Christian},
  title =	{{Principles of Contract Languages (Dagstuhl Seminar 22451)}},
  pages =	{1--27},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{11},
  editor =	{Gurov, Dilian and H\"{a}hnle, Reiner and Huisman, Marieke and Reger, Giles and Lidstr\"{o}m, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.11.1},
  URN =		{urn:nbn:de:0030-drops-178334},
  doi =		{10.4230/DagRep.12.11.1},
  annote =	{Keywords: software contracts, program specifications, software development, program analysis}
}
Document
Seventeen Provers Under the Hammer

Authors: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.

Cite as

Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
  author =	{Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
  title =	{{Seventeen Provers Under the Hammer}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
  URN =		{urn:nbn:de:0030-drops-167178},
  doi =		{10.4230/LIPIcs.ITP.2022.8},
  annote =	{Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
Document
A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462)

Authors: Klaus Havelund, Martin Leucker, Giles Reger, and Volker Stolz

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


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17462 "A Shared Challenge in Behavioural Specification". The seminar considered the issue of behavioral specification with a focus on its usage in Runtime Verification. The seminar was motivated by the observations that, whilst the field of Runtime Verification is becoming more mature, there is a lack of common specification language, in the main part due to the rich setting allowing for highly expressive languages. The aim of the Seminar was to shed light on the similarities and differences between the different existing languages, and specifically, suggest directions for future collaboration and research. The seminar consisted of two talk sessions, two working group sessions, and a feedback and reflection session. Working group topics were suggested and agreed in response to points raised in talks. One significant outcome was the proposal of a shared challenge project in which different Runtime Verification approaches can be compared, as outlined in one of the working group reports.

Cite as

Klaus Havelund, Martin Leucker, Giles Reger, and Volker Stolz. A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462). In Dagstuhl Reports, Volume 7, Issue 11, pp. 59-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Article{havelund_et_al:DagRep.7.11.59,
  author =	{Havelund, Klaus and Leucker, Martin and Reger, Giles and Stolz, Volker},
  title =	{{A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462)}},
  pages =	{59--85},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{11},
  editor =	{Havelund, Klaus and Leucker, Martin and Reger, Giles and Stolz, Volker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.11.59},
  URN =		{urn:nbn:de:0030-drops-86716},
  doi =		{10.4230/DagRep.7.11.59},
  annote =	{Keywords: behavioural specification, dynamic properties, runtime verification, temporal logic}
}
  • Refine by Author
  • 2 Reger, Giles
  • 1 Blanchette, Jasmin
  • 1 Desharnais, Martin
  • 1 Gurov, Dilian
  • 1 Havelund, Klaus
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Theory of computation → Program specifications

  • Refine by Keyword
  • 1 Automatic theorem proving
  • 1 behavioural specification
  • 1 dynamic properties
  • 1 interactive theorem proving
  • 1 program analysis
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2018
  • 1 2022
  • 1 2023

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