Go2Pins: a framework for the LTL verification of Go programs
We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin  and Spot . Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired from the hardware verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. In this paper we demonstrate the usage of Go2Pins over benchmark inspired from industrial problems and a set of LTL formulae. Even if Go2Pins is still at the early stages of development, our results are promising and show the benefits of using black-box transitions.
Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:00 - 17:00
|Go2Pins: a framework for the LTL verification of Go programs|
|C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs|
|Probabilistic Model Checking of Randomized Java Code|