Handling blackbox transitions in go2pins

From LRDE

Revision as of 13:36, 26 June 2021 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Hugo Moreau | title = Handling blackbox transitions in go2pins | year = 2021 | number = 2108 | abstract = go2pins is a tool used to interface Go progra...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

go2pins is a tool used to interface Go programs with model checking algorithms. Through a series of transformations, a standard Go program is compiled to another behaving the same way, but exposing an interface allowing to iterate over its various states. We introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approachinspired from the hardware verification techniques, allows easy, automatic and efficient abstractions. In this report, we introduce the development behind the introduction of the black-box transitions in go2pins and the problems encountered.