Student Seminar 2019-07-02
13h00 Parallelism and Indexation in Quickref – Antoine Hacquard
Quicklisp is a library manager working with your existing Common Lisp implementation to download and install around 2000 libraries, from a central archive. Quickref, an application itself written in Common Lisp, generates automatically and by introspection, a technical documentation of every libraries of Quicklisp, and produce a website from this documentation. This technical report has a vocation to summarized the work performed until now on two aspect of this library. The first one is the parallelization of Quickref whereas the second one is the creation of three new indexes (by author, by keyword and by theme), requiring the implementation of text retrieval algorithms (lexical, semantic, etc...)
13h30 Brain Tumor Segmentation with deep convolutional network approach – Thibault Buatois
Gliomas are a category of brain tumors that have different degrees of malignancy, shapes and textures. Manual segmentation by experts is a challenging task because of the heterogeneity of these tumors. Several methods of automated gliomas segmentation have been studied at MICCAI 2018 BraTS Challenge. We want to improve the segmentation results submitted last year by LRDE's team, using VGG architecture. This convolutional neural network, classically used for natural image categorization, has been adapted for medical image segmentation through transfert learning and pseudo-3D techniques. Current improvements notably focus on preprocessing, using morphological operators, and will be submitted to this year's challenge.
14h00 Binding a high-performance C++ image processing library to Python – Celian Gossec
Pylene is an image processing (IP) library aiming for high genericity and performance. To accomplish its goals, it was created using C++ templates, allowing for great flexibility and no loss of performance. Pylene is one of the few IP libraries that successfully uses templates, which means it could become a staple in the IP field, but it would first have to overcome a big issue resulting from the usage of C++ templates. That issue is the usability of the library. C++ is not known for its ease of use, and by extensionthis makes Pylene hard to use in concrete IP problems. Here, we try to overcome this problem through a Python version of the library. Seeing as though recreating all the library in Python would be nigh impossible, it seems sensible to instead try to bind the high level API to Python. This in itself brings up another issue: the available techniques do not answer our problems well enough, especially in regards to C++ template bindings. Since the idea behind templates of "knowing the type at compile time" doesn't exist in Python, we are faced with a gap between the static world of C++ templates, and the dynamic world of Python. We are presenting in this paper our solution to cross this static-dynamic difference: removing the templates through type-erasure and using contextual information for the type retrieval in Python.
14h45 Using Scatter Search to find better variable ordering in BDDs – Samuel Corno
15h15 Distributed State Space Exploration – Paul Guénézan
In the model checking field, the data structures used to represent a given program can't be stored in memory due to combinatorial explosion. To speed up the exploration of such large data structureswe can use parallel or distributed algorithms. In this report, we present an implemention of a distributed state space exploration algorithm proposed by Camille Coti in "One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters". We compare it against a synchronous algorithm and an asynchronous algorithm using threads to communicate with the same machine. We give benchmarks of all these algorithms using the BEEN benchmark.
15h45 Reimplementation of testing-automata in Spot – Martin Huvelle
Spot is a library of model checking algorithms which can manage different kinds of '"`UNIQ--math-00000005-QINU`"'-automata. It can also handle testing-automata since Spot 1.0. However, Spot 2.0 introduced a new data structure for automata with generic acceptance conditions that were not available when testing automata where developed. Our goal is to reimplement testing-automata using the more modern data structure. By doing so, we expect to reuse existing algorithms, to reduce the amount code specific to testing automata, and to make testing automata compatible with HOA format. Additionally, our preliminary implementation seems to produce smaller testing-automata than the original one.
16h15 Exploring various implementations for goroutines support in go2pins – Antoine Martin
go2pins is a tool used to interface Go programs with model checking algorithms. Through a series of transformations, a standard Go program is compiled to another behaving the same way, but exposing an interface allowing to iterate over its various states. However, go2pins currently doesn't support programs that use goroutines, Go's concurrency primitives. In this report, we present the various solutions we've assessed to implement this behaviour inside go2pins, and the problems we've had to solve along the way.