Difference between revisions of "Jobs/M2 2015 ADL Python Interfaces for Spot"
From LRDE
Line 16: | Line 16: | ||
|Contact=<adl at lrde . epita . fr> |
|Contact=<adl at lrde . epita . fr> |
||
|Compensation=1000 € gross/month |
|Compensation=1000 € gross/month |
||
− | |Future work opportunities=If you have performed the internship satisfactorily, we would like it to be followed by a PhD thesis. |
||
|Type=Master Internship |
|Type=Master Internship |
||
|Language=en |
|Language=en |
Revision as of 15:36, 12 December 2014
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 | |
Advisor | |
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:
|
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 |