Jobs/M2 2015 ADL Python Interfaces for Spot

	Development of an IPython interface, and a couple of web interfaces for the Spot library
Reference id	M2 2015 ADL Python Interfaces for Spot
Dates	5-6 months in 2015
Research field	Automata Theory
Related project	Spot
Advisor	Alexandre Duret-Lutz
General presentation of the field	The Spot library (http://spot.lip6.fr/), written in C++, offers several algorithms and data structures to build model checkers. It contains many algorithms for handling linear-time temporal logic (LTL) formulas, or for different variants of Büchi automata. Spot also distributes several command-line tools, built on top of the library. Finally, Spot includes some Python bindings, as well as a web interface (http://spot.lip6.fr/ltl2tgba.html) for easy access to one of the features of the library.
Prerequisites	This internship targets students who: have some experience in Python programming and Unix development (experience with git would be a welcome bonus) have some notions of C++ and web development
Objectives	The goal of the internship is to improve the last two points (Python bindings and web interface): we would like to access all features of Spot from Python (and in particular from IPython), and on top of this Python interface, we would like more on-line services that people can use without having to install Spot.
Benefit for the candidate
References
Place	LRDE: How to get to us
Compensation	1000 € gross/month
Future work opportunities
Contact	<adl at lrde . epita . fr> <adl at lrde . epita . fr>