3 Search Results for "Hugues, Jérôme"


Document
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users

Authors: Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)


Abstract
The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.

Cite as

Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.ITP.2023.12,
  author =	{de Almeida Borges, Ana and Casanueva Art{\'\i}s, Annal{\'\i} and Falleri, Jean-R\'{e}my and Gallego Arias, Emilio Jes\'{u}s and Martin-Dorel, \'{E}rik and Palmskog, Karl and Serebrenik, Alexander and Zimmermann, Th\'{e}o},
  title =	{{Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.12},
  URN =		{urn:nbn:de:0030-drops-183875},
  doi =		{10.4230/LIPIcs.ITP.2023.12},
  annote =	{Keywords: Coq, Community, Survey, Statistical Analysis}
}
Document
Architecture-Driven Semantic Analysis of Embedded Systems (Dagstuhl Seminar 12272)

Authors: Peter Feiler, Jérôme Hugues, and Oleg Sokolsky

Published in: Dagstuhl Reports, Volume 2, Issue 7 (2013)


Abstract
Architectural modeling of complex embedded systems is gaining prominence in recent years, both in academia and in industry. An architectural model represents components in a distributed system as boxes with well-defined interfaces, connections between ports on component interfaces, and specifies component properties that can be used in analytical reasoning about the model. Models are hierarchically organized, so that each box can contain another system inside, with its own set of boxes and connections between them. The goal of Dagstuhl Seminar 12272 ``Architecture-Driven Semantic Analysis of Embedded Systems'' is to bring together researchers who are interested in defining precise semantics of an architecture description language and using it for building tools that generate analytical models from architectural ones, as well as generate code and configuration scripts for the system. This report documents the program and the outcomes of the presentations and working groups held during the seminar.

Cite as

Peter Feiler, Jérôme Hugues, and Oleg Sokolsky. Architecture-Driven Semantic Analysis of Embedded Systems (Dagstuhl Seminar 12272). In Dagstuhl Reports, Volume 2, Issue 7, pp. 30-55, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@Article{feiler_et_al:DagRep.2.7.30,
  author =	{Feiler, Peter and Hugues, J\'{e}r\^{o}me and Sokolsky, Oleg},
  title =	{{Architecture-Driven Semantic Analysis of Embedded Systems (Dagstuhl Seminar 12272)}},
  pages =	{30--55},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{2},
  number =	{7},
  editor =	{Feiler, Peter and Hugues, J\'{e}r\^{o}me and Sokolsky, Oleg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.7.30},
  URN =		{urn:nbn:de:0030-drops-37343},
  doi =		{10.4230/DagRep.2.7.30},
  annote =	{Keywords: Architectu Description Language, AADL, EAST-ADL, MARTE, Verification, Validation, Analysis, Embedded Systems, Model-Driven techniques}
}
Document
Applying WCET Analysis at Architectural Level

Authors: Olivier Gilles and Jérôme Hugues

Published in: OASIcs, Volume 8, 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08) (2008)


Abstract
Real-Time embedded systems must enforce strict timing constraints. In this context, achieving precise Worst Case Execution Time is a prerequisite to apply scheduling analysis and verify system viability. WCET analysis is usually a complex and time-consuming activity. It becomes increasingly complex when one also considers code generation strategies from high-level models. In this paper, we present an experiment made on the coupling of the WCET analysis tool Bound-T and our AADL to code generator OCARINA. We list the different steps to successfully apply WCET analysis directly from model, to limit user intervention.

Cite as

Olivier Gilles and Jérôme Hugues. Applying WCET Analysis at Architectural Level. In 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08). Open Access Series in Informatics (OASIcs), Volume 8, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{gilles_et_al:OASIcs.WCET.2008.1665,
  author =	{Gilles, Olivier and Hugues, J\'{e}r\^{o}me},
  title =	{{Applying WCET Analysis at Architectural Level}},
  booktitle =	{8th International Workshop on Worst-Case Execution Time Analysis (WCET'08)},
  pages =	{1--9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-10-1},
  ISSN =	{2190-6807},
  year =	{2008},
  volume =	{8},
  editor =	{Kirner, Raimund},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2008.1665},
  URN =		{urn:nbn:de:0030-drops-16653},
  doi =		{10.4230/OASIcs.WCET.2008.1665},
  annote =	{Keywords: WCET, AADL, Bound-T, Ocarina}
}
  • Refine by Author
  • 2 Hugues, Jérôme
  • 1 Casanueva Artís, Annalí
  • 1 Falleri, Jean-Rémy
  • 1 Feiler, Peter
  • 1 Gallego Arias, Emilio Jesús
  • Show More...

  • Refine by Classification
  • 1 General and reference → Empirical studies
  • 1 Software and its engineering → Formal methods

  • Refine by Keyword
  • 2 AADL
  • 1 Analysis
  • 1 Architectu Description Language
  • 1 Bound-T
  • 1 Community
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2008
  • 1 2012
  • 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