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

Handle with Care and Confidence – Extending Cameleer with Algebraic Effects and Effect Handlers. An analysis of algebraic effects and techniques to deductively verify them

Autor: Soares, Tiago Lopes

The new major release of the OCaml compiler is set to be an important landmark in the history and ecosystem of the language. The 5.0 version introduces Multicore OCaml, a multi-threaded implementation of the OCaml runtime. Two new important paradigms

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______1437::3b2dbb11af01b1e12b98dfe6f485bc56
https://hdl.handle.net/10362/151098

Verification of distributed algorithms with the Why3 tool

Autor: Cruz, Carla Isabel Novais

Dissertação de mestrado integrado em Informatics Engineering
Nowadays, there currently exist many working program verification tools however, the developed tools are mostly limited to the verification of sequential code, or else of multi-threa

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______307::95bd36328dbb79badbf440453d3b4665
https://hdl.handle.net/1822/80033

Une sémantique à pas de géant pour la catégorisation des contre-exemples

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

Publikováno v: [Research Report] RR-9407, Inria. 2021, pp.43
HAL

Deductive Verification aims at verifying that a given program code conforms to a formal specification of its intended behaviour. That approachproceeds by generating mathematical statements whose validity entails the conformance of the program. Such s

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::5063f7820de24ae11d7498756bbeae08
https://inria.hal.science/hal-03213438/document

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