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

My documents

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.