Zobrazeno 1 - 10 of 12 pro vyhledávání: '"Martin Clochard"'
1
Akademický článek
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
Zobrazit plný text záznamu
2
Gobra: Modular Specification and Verification of Go Programs
Autor: Peter Müller, Felix A. Wolf, Wytse Oortwijn, Martin Clochard, João C. Pereira, Linard Arquint
Publikováno v: Lecture Notes in Computer Science, 12759
Computer Aided Verification, 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I
Computer Aided Verification ISBN: 9783030816841
CAV (1)
Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through gorout
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fe9a231f0daa7feab3203856853581d7
https://hdl.handle.net/20.500.11850/511854
Zobrazit plný text záznamu
3
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Autor: David Basin, Peter Müller, Felix A. Wolf, Christoph Sprenger, Tobias Klenze, Martin Clochard, Marco Eilers
Publikováno v: arXiv
Proceedings of the ACM on Programming Languages, 4 (OOPSLA)
Lighthouse projects like CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full system verification is feasible by establishing a refinement between an abstract system specification and an executable implementation. Existing approaches h
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::71409a177628bff68b49d687cde86a4e
https://hdl.handle.net/20.500.11850/458115
Zobrazit plný text záznamu
4
Deductive Verification with Ghost Monitors
Autor: Claude Marché, Andrei Paskevich, Martin Clochard
Publikováno v: POPL 2020-47th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2020-47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩
Proceedings of the ACM on Programming Languages, 4 (POPL)
We present a new approach to deductive program verification based on auxiliary programs called ghost monitors. This technique is useful when the syntactic structure of the target program is not well suited for verification, for example, when an essen
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d9418ce674f4cf7ac07a7422b3543b9d
Zobrazit plný text záznamu
5
The Matrix Reproved (Verification Pearl)
Autor: Mário Pereira, Martin Clochard, Léon Gondelman
Publikováno v: Lecture Notes in Computer Science ISBN: 9783319488684
VSTTE
In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops a
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b9643498edb90670e6e6bda86076562b
https://doi.org/10.1007/978-3-319-48869-1_8
Zobrazit plný text záznamu
6
The Matrix Reproved (Verification Pearl)
Autor: Léon Gondelman, Mário Pereira, Martin Clochard
Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2018, 60 (3), pp.365-383. ⟨10.1007/s10817-017-9436-2⟩
VSTTE 2016
VSTTE 2016, Jul 2016, Toronto, Canada
HAL
CIÊNCIAVITAE
Journal of Automated Reasoning, 2018, 60 (3), pp.365-383. ⟨10.1007/s10817-017-9436-2⟩
International audience; In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version us
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::892add359417a5d992d54e372719fb9b
https://hal.inria.fr/hal-01316902v2
Zobrazit plný text záznamu
7
How to avoid proving the absence of integer overflows
Autor: Jean-Christophe Filliâtre, Martin Clochard, Andrei Paskevich
Publikováno v: 7th Working Conference on Verified Software: Theories, Tools, and Experiments
7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States
Lecture Notes in Computer Science ISBN: 9783319296128
VSTTE
International audience; When proving safety of programs, we must show, in particular, the absence of integer overflows. Unfortunately, there are lots of situations where performing such a proof is extremely difficult, because the appropriate restrict
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::50f0266a4316733d496207d791a41c52
https://hal.inria.fr/hal-01162661v2/file/main.pdf
Zobrazit plný text záznamu
8
Formalizing Semantics with an Automatic Program Verifier
Autor: Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
Publikováno v: 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)
6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
HAL
International audience; A common belief is that formalizing semantics of programming languages requires the use of a proof assistant providing (1) a specification language with advanced features such as higher-order logic, inductive definitions, type
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::d367d1a44b96ed9dd397a6307da36751
https://hal.inria.fr/hal-01067197/document
Zobrazit plný text záznamu
9
Formalizing Semantics with an Automatic Program Verifier
Autor: Andrei Paskevich, Claude Marché, Martin Clochard, Jean-Christophe Filliâtre
Publikováno v: Verified Software: Theories, Tools and Experiments ISBN: 9783319121536
VSTTE
A common belief is that formalizing semantics of programming languages requires the use of a proof assistant providing (1) a specification language with advanced features such as higher-order logic, inductive definitions, type polymorphism, and (2) a
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::eb09fb9fd127de8aefda310b4deee384
https://doi.org/10.1007/978-3-319-12154-3_3
Zobrazit plný text záznamu
10
Verified Programs with Binders
Autor: Claude Marché, Andrei Paskevich, Martin Clochard
Publikováno v: Programming Languages meets Program Verification
Programming Languages meets Program Verification, Jan 2014, San Diego, United States
HAL
PLPV
International audience; Programs that treat datatypes with binders, such as theorem provers or higher-order compilers, are regularly used for mission-critical purposes, and must be both reliable and performant. Formally proving such programs using as
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8872c9277fd0aac7d67cdb39c18a1d14
https://hal.inria.fr/hal-00913431/document
Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání

Omezení vyhledávání
Plný text Recenzováno Digitální knihovna AV ČR
Zdroje