Difference between revisions of "Publications/moreau.21.seminar"
From LRDE
(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...") |
|||
| Line 4: | Line 4: | ||
| year = 2021 |
| year = 2021 |
||
| number = 2108 |
| number = 2108 |
||
| − | | 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 |
+ | | 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 reportwe introduce the development behind the introduction of the black-box transitions in textttgo2pins and the problems encountered. |
| type = techreport |
| type = techreport |
||
| id = moreau.21.seminar |
| id = moreau.21.seminar |
||
Latest revision as of 15:45, 10 March 2022
- Authors
- Hugo Moreau
- Type
- techreport
- Year
- 2021
- Number
- 2108
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 reportwe introduce the development behind the introduction of the black-box transitions in textttgo2pins and the problems encountered.