Dear all,
I am pleased to announce my habilitation defense, entitled
(dynamic (programming paradigms)) ;; performance and expressivity
to be held on Friday, July 10, 14:00 CEST. Due to the current pandemic,
the defense will take place on a Zoom public channel. The actual link to
the video-conference will be provided later on, at the following URL:
https://www.lrde.epita.fr/~didier/research/publications/papers.php#verna.20…
The jury is composed as follows.
Reporters:
Robert Strandh, University of Bordeaux, France
Nicolas Neuß, FAU, Erlangen-Nürnberg, Germany
Manuel Serrano, INRIA, Sophia Antipolis, France
Examiners:
Marco Antoniotti, University of Milan, Italy
Ralf Möller, Université of Lübech, Germany
Gérard Assayag, IRCAM, Paris, France
--
Resistance is futile. You will be jazzimilated.
Lisp, Jazz, Aïkido: http://www.didierverna.info
Greetings,
We are please to announce that the following paper has been accepted for publication in "Innovations in Systems and Software Engineering: a NASA journal (ISSE)".
Title and corresponding authors:
"Improving swarming using genetic algorithms"
Etienne Renault (1)
(1) LRDE, EPITA, Le Kremlin-Bicêtre, France
Abstract:
The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increase performance. Nonetheless, the topology of the state space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation is 10% faster than state-of-the-art algorithms on a general benchmark and 40% on a specialized benchmark. Even if we expected a decrease in an order of magnitude, these results are still encouraging since they suggest a new way to handle existing limitations. Empirically, our technique seems well suited for "linear topology", i.e., the one we can obtain when combining model checking algorithms with partial-order reduction techniques.
More information at :
https://www.lrde.epita.fr/wiki/Publications/renault.20.isse <https://www.lrde.epita.fr/wiki/Publications/renault.20.isse>
