Maximilien Colange

From Spot 2.0 to Spot 2.10: What’s new?

By Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko

2022-06-06

In Proceedings of the 34th international conference on computer aided verification (CAV’22)

Abstract Spot is a C++17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more.

Continue reading

The reactive synthesis competition (SYNTCOMP): 2018-2021

By Swen Jacobs, Guillermo Alberto Perez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara J. Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clément Tamines, Leander Tentrup, Adam Walker

2022-06-01

In

Abstract

Continue reading

Reactive synthesis from LTL specification with Spot

By Thibaud Michaud, Maximilien Colange

2018-06-07

In Proceedings of the 7th workshop on synthesis, SYNT@CAV 2018

Abstract We present ltlsynt, a new tool for reactive synthesis from LTL specifications. It relies on the efficiency of Spot to translate the input LTL specification to a deterministic parity automaton. The latter yields a parity game, which we solve with Zielonka’s recursive algorithm.The approach taken in ltlsynt was widely believed to be impractical, due to the double-exponential size of the parity game, and to the open status of the complexity of parity games resolution.

Continue reading

CDCLSym: Introducing effective symmetry breaking in SAT solving

By Hakan Metin, Souheib Baarir, Maximilien Colange, Fabrice Kordon

2018-01-05

In Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS’18)

Abstract SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones.

Continue reading

The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results

By Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur, Leander Tentrup

2017-07-01

In Proceedings sixth workshop on synthesis

Abstract

Continue reading

Programmatic manipulation of Common Lisp type specifiers

By Jim Newton, Didier Verna, Maximilien Colange

2017-02-06

In ELS 20217, the 10th european lisp symposium

Abstract In this article we contrast the use of the s-expression with the BDD (Binary Decision Diagram) as a data structure for programmatically manipulating Common Lisp type specifiers. The s-expression is the de facto standard surface syntax and also programmatic representation of the type specifier, but the BDD data structure offers advantages: most notably, type equivalence checks using s-expressions can be computationally intensive, whereas the type equivalence check using BDDs is a check for object identity.

Continue reading

Search

Tags