A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links

Autor: Ran Chen, Martin Clochard, Claude Marché

Publikováno v: Journal of Formalized Reasoning, Vol 10, Iss 1, Pp 51-66 (2017)

In the context of file systems like those of Unix, path resolution is the operation that given a character string denoting an access path, determines the target object (a file, a directory, etc.) designated by this path. This operation is not trivial

Externí odkaz: https://doaj.org/article/4f820c8915b949288a33969f3c6911c2

Automated Formal Analysis of Temporal Properties of Ladder Programs

Autor: Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue

Publikováno v: International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩

International audience; Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this wo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7e33021b1b500f86b72d06a08ea446a3
https://inria.hal.science/hal-03737869/document

Explaining Counterexamples with Giant-Step Assertion Checking

Autor: Claude Marché, Cláudio Belo Lourenço, Benedikt Becker

Publikováno v: F-IDE 2021-6th Workshop on Formal Integrated Development Environments
F-IDE 2021-6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨10.4204/EPTCS.338.10⟩
HAL

Identifying the cause of a proof failure during deductive verification of programs is hard: it may be due to an incorrectness in the program, an incompleteness in the program annotations, or an incompleteness of the prover. The changes needed to reso

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::57ad2fff503153589b85a40b7ceaf056
https://hal.inria.fr/hal-03217393/document

You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3

Autor: Diego Diverio, Cláudio Belo Lourenço, Claude Marché

Publikováno v: VerifyThis 2020-Long-term Challenge
VerifyThis 2020-Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7
HAL

International audience; We report on a solution we designed for the VerifyThis Collaborative Long Term Challenge 2019. We used the Why3 verification framework to design, from scratch, a simple but running prototype implementation of a PGP key server.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::9520b26e5197eaecaad7252925450894
https://inria.hal.science/hal-03002187

Analysing installation scenarios of Debian packages

Autor: Mihaela Sighireanu, Nicolas Jeannerod, Claude Marché, Ralf Treinen, Yann Régis-Gianas, Benedikt Becker

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030452360
TACAS (2)
Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2020-26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2020-26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩

The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in Posix shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::83781a0aa95ff8ec80f03f0f0b2d4b88
https://doi.org/10.1007/978-3-030-45237-7_14