Antoine Martin

In International Journal on Software Tools for Technology Transfer (STTT)

Abstract 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 by hardware verification techniques, allows easy, automatic and efficient abstractions.

From Spot 2.0 to Spot 2.10: What’s new?

By Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko

2022-06-06

In Proceedings of the 34th international conference on computer aided verification (CAV’22)

Abstract Spot is a C++17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more.

Go2Pins: A framework for the LTL verification of Go programs

By Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Étienne Renault

2021-06-08

In Proceedings of the 27th international SPIN symposium on model checking of software (SPIN’21)

Abstract We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is an effort to promote the integration of both formal verifica- tion 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 by hardware ver- ification techniques, allows easy, automatic and efficient abstractions.

Go2Pins: A framework for the LTL verification of Go programs (extended version)

From Spot 2.0 to Spot 2.10: What’s new?

Go2Pins: A framework for the LTL verification of Go programs

Search

Tags