Výsledky vyhledávání - "Julien Braine"

Data Abstraction: A General Framework to Handle Program Verification of Data Structures

Autor: Laure Gonnord, Julien Braine, David Monniaux

Publikováno v: [Research Report] RR-9408, Inria Grenoble Rhône-Alpes; VERIMAG UMR 5104, Université Grenoble Alpes, France; LIP-Laboratoire de l’Informatique du Parallélisme; Université Lyon 1-Claude Bernard; ENS Lyon. 2021, pp.1-29
Static Analysis ISBN: 9783030888053
SAS
SAS 2021-28th Static Analysis Symposium
SAS 2021-28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.215-235, ⟨10.1007/978-3-030-88806-0_11⟩
HAL

Proving properties on programs accessing data structures such as arrays often requires universally quantified invariants, e.g., "all elements below index $i$ are nonzero''. In this research report, we propose a general data abstraction scheme operati

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

Zobrazit plný text záznamu

Proving array properties using data abstraction

Autor: Laure Gonnord, Julien Braine

Publikováno v: Numerical and Symbolic Abstract Domains (NSAD)
Numerical and Symbolic Abstract Domains (NSAD), Nov 2020, Virtual, United States
[Research Report] ENS Lyon, CNRS & INRIA. 2020

This paper presents a framework to abstract data structures within Horn clauses that allows abstractions to be easily expressed, compared, composed and implemented. These abstractions introduce new quantifiers that we eliminate with quantifier elimin

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0efae7f22c3cbd87a7b78a0079f16b72
https://hal.science/hal-02948081v2/document

Zobrazit plný text záznamu

Verifying Programs with Arrays and Lists

Autor: Julien Braine, Laure Gonnord, David Monniaux

Publikováno v: HAL
[Internship report] ENS Lyon. 2016

Automatically verifying safety properties of programs is a tough problem that has been tackled using many different approaches: rewriting systems, abstract interpretation, SMT solving,. .. Most techniques restrict themselves to programs operating on

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::e258ed66153a9eb7c69c9203bd47220f
https://hal.archives-ouvertes.fr/hal-01337140

Zobrazit plný text záznamu

Elektronická kniha

Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I

Autor: Isil Dillig, Serdar Tasiran

This open access two-volume set LNCS 11561 and 11562 constitutes the refereed proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019, held in New York City, USA, in July 2019. The 52 full papers presented together w

Zobrazit plný text záznamu

Elektronická kniha

Static Analysis : 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings

Autor: Cezara Drăgoi, Suvam Mukherjee, Kedar Namjoshi

This book constitutes the refereed proceedings of the 28th International Symposium on Static Analysis, SAS 2021, held in Chicago, IL, USA, in October 2021.The 18 regular and 4 short papers, carefully reviewed and selected from 48 submissions, are pre

Zobrazit plný text záznamu

Elektronická kniha

Automated Reasoning with Analytic Tableaux and Related Methods : 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings

Autor: Serenella Cerrito, Andrei Popescu

This book constitutes the proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, held in London, UK, in September 2019, colocated with the 12th International Symposium on Fro

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání