Exploiting Pointer Analysis in Memory Models for Deductive Verification

Autor: Quentin, Bouillaguet, François, Bobot, Mihaela, Sighireanu, Boris, Yakobowski

Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer

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

Analysing installation scenarios of Debian packages

Autor: Mihaela Sighireanu, Nicolas Jeannerod, Claude Marché, Ralf Treinen, Yann Régis-Gianas, Benedikt Becker

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030452360
TACAS (2)
Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2020-26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2020-26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩

The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in Posix shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::83781a0aa95ff8ec80f03f0f0b2d4b88
https://doi.org/10.1007/978-3-030-45237-7_14

SL-COMP: Competition of Solvers for Separation Logic

Autor: Adam Rogalewicz, Chong Gao, Michal Cyprian, Juan Antonio Navarro Pérez, Quang-Trung Ta, Wei-Ngan Chin, Mihaela Sighireanu, Nikos Gorogiannis, Tomáš Vojnar, Thomas Noll, Andrew Reynolds, Ondrej Lengál, Ton Chanh Le, Quang Loc Le, Constantin Enea, Andrey Rybalchenko, Jens Katelaan, Thanh-Toan Nguyen, Zhilin Wu, Christoph Matheja, Siau-Cheng Khoo, Radu Iosif, Florian Zuleger, Cristina Serban

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems-25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019
Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TOOLympics, Held as Part of 2019, Apr 2019, Prague, Czech Republic. pp.116-132, ⟨10.1007/978-3-030-17502-3_8⟩
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030175016
TACAS (3)

International audience; SL-COMP aims at bringing together researchers interested on improving the state of the art of the automated deduction methods for Separation Logic (SL). The event took place twice until now and collected more than 1K problems

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::430f3459dc4dd84c205e9a65fbc661b3
https://hal.archives-ouvertes.fr/hal-02388022

Report on SL-COMP 2014

Autor: Mihaela Sighireanu, David R. Cok

Publikováno v: Journal on Satisfiability, Boolean Modeling and Computation. 9:173-186

A competition of solvers for Separation Logic was held in May 2014, as an unofficial satellite event of the FLoC Olympic Games. Six solvers participated in the competition; the success and performance of each solver was measured over an appropriate s

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e02679aa1966561fc3a269d99075c8ae
https://doi.org/10.3233/sat190107

A Verified Implementation of the Bounded List Container

Autor: Raphaël Cauderlier, Mihaela Sighireanu

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783319899596
TACAS (1)

This paper contributes to the trend of providing fully verified container libraries. We consider an implementation of the bounded doubly linked list container which manages the list in a fixed size, heap allocated array. The container provides consta

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::f5b826c4ed3edda24a29e21b4cde2393
https://doi.org/10.1007/978-3-319-89960-2_10