Výsledky vyhledávání - "Hurlin, Clément"

Report

Permission-Based Separation Logic for Multithreaded Java Programs

Autor: Haack, Christian, Huisman, Marieke, Hurlin, Clément, Amighi, Afshin

Publikováno v: Logical Methods in Computer Science, Volume 11, Issue 1 (February 27, 2015) lmcs:998

This paper presents a program logic for reasoning about multithreaded Java-like programs with dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed adaptatio

Externí odkaz: http://arxiv.org/abs/1411.0851

Zobrazit plný text záznamu

Semi-Automatic Synthesis of Security Policies by Invariant-Guided Abduction - Full version

Autor: Hurlin, Clément, Kirchner, Helene

Publikováno v: [Research Report] 2010, pp.19

We present a specification approach of secured systems as transition systems and security policies as constraints that guard the transitions. In this context, security properties are expressed as invariants. Then we propose an abduction algorithm to

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::e7d3834bd5beed248784c0562f9bdd9c
https://inria.hal.science/inria-00507754

Zobrazit plný text záznamu

Permission Specifications for Common Multithreaded Programming Patterns

Autor: Huisman, Marieke, Hurlin, Clément

Publikováno v: Book in the honor of Henk Barendregt for his 60th birthday
Book in the honor of Henk Barendregt for his 60th birthday, Dec 2007, Nimègue, Netherlands

National audience; Multithreading is the next challenge for program verification. To support modular verification of multithreaded programs, one should know when data might be accessed or updated by the different threads in the system. We propose a p

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::2cd497a8462583de9739d082b102589c
https://inria.hal.science/inria-00204771/file/henk.pdf

Zobrazit plný text záznamu

Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions

Autor: Hurlin, Clément, Chaib, Amine, Fontaine, Pascal, Merz, Stephan, Weber, Tjark

Publikováno v: The Isabelle Workshop 2007-Isabelle'07
The Isabelle Workshop 2007-Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13

URL : http://homepages.inf.ed.ac.uk/ldixon/events/isabelle-ws-07/isabelle-07.pdf; International audience; Proof reconstruction is a technique that combines an interactive theorem prover and an automatic one in a sound way, so that users benefit from

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::3a15a2ff1962e71724771c8eee2e2a7f
https://hal.inria.fr/inria-00186638

Zobrazit plný text záznamu

Proof reconstruction for first-order logic and set-theoretical constructions

Autor: Hurlin, Clément

Publikováno v: Automatic Verification of Critical Systems-AVoCS 2006
Automatic Verification of Critical Systems-AVoCS 2006, Sep 2006, Nancy/France, pp.157-162

Proof reconstruction is a technique that combines an interactive theorem prover and an automatic one in a sound way, so that users benefit of the expressiveness of the first tool and the automation of the latter. We present an implementation for proo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::5e972737568ddd005b4348be5ed9fcc6
https://hal.inria.fr/inria-00091811

Zobrazit plný text záznamu

Reconstruction de preuves pour les formules quantifiées et ensemblistes

Autor: Hurlin, Clément

Publikováno v: [Travaux universitaires] 2006, pp.29-VII

Stage effectué au Loria et à l'Université Technique de Munich; La reconstruction de preuve est une technique qui combine un prouveur interactif et un prouveur automatique de manière correcte. L'utilisateur bénéficie ainsi de l'expressivité du

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______165::6e0c19465830e9e53bcaccbfbc506ac5
https://inria.hal.science/inria-00212213/file/mr2.pdf

Zobrazit plný text záznamu