Go2Pins
This is my current work as a Research Student at LRDE (EPITA Research and Development Laboratory). I’m supervised by Etienne Renault. Go2Pins is accesible here.
We present Go2Pins, a tool that takes a program written in Go and links it with an ecosystem of model-checkers. To handle efficiently the Go runtime, we introduce blackbox transitions: a combination between transpilation techniques and approaches inspired from the hardware verification realm. Besides Go2Pins, we also propose LTL Rec, an extra tool that aims to simplify the expression of LTL properties over Go programs. A benchmark inspired from industrial problems show the validity of our approach and the benefits of using blackbox transitions.
Recruiting procedure
During my recruitment, I have been asked to read this paper : A static verification framework for message passing in go using behavioural types.
This work proposes a practical verification framework for message passing concurrency in Go by developing a robust static analysis that infers an abstract model of a program’s communicationbehaviour in the form of a behavioural type, a powerful processcalculi typing discipline. We make use of our analysis to deploy amodel and termination checking based verification of the inferredbehavioural type that is suitable for a range of safety and livenessproperties of Go programs, providing several improvements overexisting approaches. We evaluate our framework and its implementation on publicly available real-world Go code.
Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida
My Work
- 2021’s 6th and 7th weeks’ summary
- 2021’s 8th week’s summary
- 2021’s 9th week’s summary
- 2021’s 10th week’s summary
- 2021’s 12th week’s summary
- 2021’s 13th week’s summary
My documents
- Recruiting procedure January 2021
- Lightning Talk February 2021
- Lightning Talk March 2021
- Lightning Talk May 2021
- Seminar July 2021
References
- Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. AStatic Verification Framework for Message Passing in Go using BehaviouralTypes. InICSE ’18: ICSE ’18: 40th International Conference on Software En-gineering , May 27-June 3, 2018, Gothenburg, Sweden.ACM, New York, NY,USA, 12 pages. https://doi.org/10.1145/3180155.3180157
- Kripke, Saul, 1963, “Semantical Considerations on Modal Logic,” Acta Philosophica Fennica, 16: 83-94
- Alur R., Bouajjani A., Esparza J. (2018) Model Checking Procedural Programs. In: Clarke E., Henzinger T., Veith H., Bloem R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_17
- Clarke E.M., Klieber W., Nováček M., Zuliani P. (2012) Model Checking and the State Explosion Problem. In: Meyer B., Nordio M. (eds) Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science, vol 7682. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35746-6_1
- Clarke, Edmund M. (2008): The Birth of Model Checking. in: Grumberg, Orna and Veith, Helmut eds.: 25 Years of Model Checking, Vol. 5000: Lecture Notes in Computer Science. Springer Berlin Heidelberg, p. 1-26.