Séminaires
Séminaire du 31 mars 2017
Lieu
LIP6, salle 24-25/405. Instructions pour venir ici.
Programme
14h00-15h00: Tali Sznajder (LIP6), "Formal methods for mobile anonymous robots"
Abstract : 
Recent advances in distributed computing highlight models and algorithms for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular,
a recent trend is the study of robots evolving in a discrete space with a finite number of locations. This discrete space is modeled by a graph, where nodes represent locations or sites, and edges represent the possibility for a robot to move from one site to another. Usually, the algorithms are handmade and designed for a parameterized number of anonymous robots, which make them difficult to prove. In this talk we will show how the use of formal methods to automatically verify or synthesize such algorithms can be beneficial, as well as the limits of such an approach.
15h00-15h30 : Ludovic Le frioux(LIP6 & LRDE), "GP-SAT: a Framework for Parallel SAT Solving"
Abstract : Over the last decade, parallelization of SAT resolution has been widely studied from both theoretical and practical aspects. There are now numerous solvers that differ by parallelization strategies, programming languages, involved libraries, programmers skills, etc.
Hence, comparing the efficiency of the (theoretical) approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool.
GP-SAT, a framework to build parallel SAT solvers for multi-cores environments, tries to solve these problems. It supports the basics of parallel SAT solvers like clause exchange, Portfolio and Divide-and-Conquer strategies. It allows users to easily create their own parallel solvers based on new strategies thanks to its genericity and modularity. Our experiments show that our framework compares well face to other different state-of-the-art solvers.