The goal of the internship is to write a translator from GO to the API in C (called PINS) developed by the ltsmin team. The PINS interface is already interfaced with Spot so the main challenge of the internship will be to proposed translation from Go structures to C.
The following steps should help you to discover and setup the environment you will work with.
- Let met know when you are registered, so that I can give you grants and setup the git repository for your internship
- Download GO from https://golang.org
- Take the Tour https://tour.golang.org/welcome/1
- While you are taking the tour, build the set of test. The most important is to write simple tests with only the "main" and the different control structures. Keep tests s simple as possible with only one concept per test. This will help us to detect errors and to ensure non-regressions.
- Have a look to go/ast to understand how you can extract all variable from your simple tests program
FYI there are few, but some, people that try to model check go program. You can have a look to this webpage: https://nickng.github.io/projects/golang/
You can also have a look to http://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/ltsmin-dve.ipynb to have an idea of what we can do with Spot through the PINS interface. The input langage is DVE which is a formal langage.
[Updated 2 Feb. 2018]
- You have to fix the subset of Go we will focus on, so that you can build a set of tests for your translater.
- Install Spot (optional)
- Install divine2 following instruction in spot/tests/ltsmin/README.
You can now run
divine compile --ltsmin model.dvethis will produce 2 files: one *.cpp one *.dve2C. Have a look to the first one to understand how to convert a program from a model.
You asked me more information about model checking. Your can have a look to my Ph.D. dissertation here
https://www.lrde.epita.fr/~renault/phd/data/renault.phd.pdf. Chapter 1 and section 2 are probably the most relevant for understanding the global approach.
@vtourneur told us that you can have troubles compiling divine. I remember no such thing but you can (1) ask help to @vtourneur or use