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

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Improving Performance of the VerCors Program Verifier

Autor: Mulder, Henk, Huisman, Marieke, Joosten, Sebastiaan, Ahrendt, Wolfgang, Beckert, Bernhard, Bubel, Richard, Hähnle, Reiner, Ulbrich, Mattias

Publikováno v: Lecture Notes in Computer Science ISBN: 9783030643539
20 Years of KeY
Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY, 65-82
STARTPAGE=65;ENDPAGE=82;TITLE=Deductive Software Verification: Future Perspectives

As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::43667017ea52c7330b239fceeb100f8c
https://doi.org/10.1007/978-3-030-64354-6_3

How to Get an Efficient yet Verified Arbitrary-Precision Integer Library

Autor: Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond

Publikováno v: 9th Working Conference on Verified Software: Theories, Tools, and Experiments
9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩
Lecture Notes in Computer Science ISBN: 9783319723075
VSTTE

International audience; The GNU Multi-Precision library is a widely used, safety-critical, library for arbitrary-precision arithmetic. Its source code is written in C and assembly, and includes intricate state-of-the-art algorithms for the sake of hi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::37e47fedf3db98f5cd6326fd62d26044
https://hal.inria.fr/hal-01519732

An Auto-active Approach to Develop Correct Logic-based Graph Transformations

Autor: Makhlouf, Amani, Percebois, Christian, Tran, Hanh Nhi

Publikováno v: International Journal On Advances in Software
International Journal On Advances in Software, IARIA, 2018, 11 (1 & 2), pp.147-158

International audience; We aim at assisting developers to write, in a Hoare style, provably correct graph transformations expressed in the ALCQ Description Logic. Given a postcondition and a transformation rule, we compute the weakest precondition fo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::643c41fa1fd42b6c23a0b6b1ca0ec087
https://hal.archives-ouvertes.fr/hal-02089337/document