2 Search Results for "Portet, Francois"

Document
DOI: 10.4230/LIPIcs.ITP.2025.24
Formally Verifying a Vertical Cell Decomposition Algorithm

Authors: Yves Bertot and Thomas Portet

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The broad context of this work is the application of formal methods to geometry and robotics. We describe an algorithm to decompose a working area containing obstacles into a collection of safe cells and the formal proof that this algorithm is correct. We expect such an algorithm will be useful to compute safe trajectories. To our knowledge, this is one of the first formalization of such an algorithm to decompose a working space into elementary cells that are suitable for later applications, with the proof of correctness that guarantees that large parts of the working space are safe. Techniques to perform this proof go from algebraic reasoning on coordinates and determinants to sorting. The main difficulty comes from the possible existence of degenerate cases, which are treated in a principled way.
Cite as

Yves Bertot and Thomas Portet. Formally Verifying a Vertical Cell Decomposition Algorithm. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2025.24,
  author =	{Bertot, Yves and Portet, Thomas},
  title =	{{Formally Verifying a Vertical Cell Decomposition Algorithm}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.24},
  URN =		{urn:nbn:de:0030-drops-246222},
  doi =		{10.4230/LIPIcs.ITP.2025.24},
  annote =	{Keywords: Formal Verification, Motion planning, algorithmic geometry}
}
Document
DOI: 10.4230/OASIcs.CMN.2014.13
A Task Based model for Récit Generation from Sensor Data: An Early Experiment

Authors: Belén A. Baez Miranda, Sybille Caffiau, Catherine Garbay, and Francois Portet

Published in: OASIcs, Volume 41, 2014 Workshop on Computational Models of Narrative

Abstract
Automatic story generation is the subject of a growing research effort. However, in this domain, stories are generally produced from fictional data. In this paper, we present a task model used for automatic story generation from real data focusing on the narrative planning. The aim is to generate récits (stories) from sensors data acquired during a ski sortie. The model and some preliminary analysis are presented which suggest the interest of the approach.
Cite as

Belén A. Baez Miranda, Sybille Caffiau, Catherine Garbay, and Francois Portet. A Task Based model for Récit Generation from Sensor Data: An Early Experiment. In 2014 Workshop on Computational Models of Narrative. Open Access Series in Informatics (OASIcs), Volume 41, pp. 13-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{baezmiranda_et_al:OASIcs.CMN.2014.13,
  author =	{Baez Miranda, Bel\'{e}n A. and Caffiau, Sybille and Garbay, Catherine and Portet, Francois},
  title =	{{A Task Based model for R\'{e}cit Generation from Sensor Data: An Early Experiment}},
  booktitle =	{2014 Workshop on Computational Models of Narrative},
  pages =	{13--23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-71-2},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{41},
  editor =	{Finlayson, Mark A. and Meister, Jan Christoph and Bruneau, Emile G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.CMN.2014.13},
  URN =		{urn:nbn:de:0030-drops-46424},
  doi =		{10.4230/OASIcs.CMN.2014.13},
  annote =	{Keywords: narrative generation, task model, real world story analysis, ambient intelligence}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2014

  • Refine by Author
  • 1 Baez Miranda, Belén A.
  • 1 Bertot, Yves
  • 1 Caffiau, Sybille
  • 1 Garbay, Catherine
  • 1 Portet, Francois
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 1 Theory of computation → Computational geometry
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Formal Verification
  • 1 Motion planning
  • 1 algorithmic geometry
  • 1 ambient intelligence
  • 1 narrative generation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact