|
| 1 | +cff-version: 1.2.0 |
| 2 | +message: Please use the bibtex in the README to cite this work |
| 3 | +title: 'GraphRedex: Look at your research' |
| 4 | +doi: 10.1002/spe.2959 |
| 5 | +authors: |
| 6 | + - family-names: Gurdeep Singh |
| 7 | + given-names: Robbert |
| 8 | + affiliation: Ghent University |
| 9 | + - family-names: Scholliers |
| 10 | + given-names: Christophe |
| 11 | + affiliation: Ghent University |
| 12 | +identifiers: |
| 13 | + - description: Research paper you should be citing |
| 14 | + type: doi |
| 15 | + value: 10.1002/spe.2959 |
| 16 | + - type: url |
| 17 | + value: https://redex.ugent.be |
| 18 | + description: Public demo site of GraphRedex |
| 19 | +preferred-citation: |
| 20 | + authors: |
| 21 | + - family-names: Gurdeep Singh |
| 22 | + given-names: Robbert |
| 23 | + affiliation: Ghent University |
| 24 | + - family-names: Scholliers |
| 25 | + given-names: Christophe |
| 26 | + affiliation: Ghent University |
| 27 | + title: 'GraphRedex: Look at your research' |
| 28 | + doi: 10.1002/spe.2959 |
| 29 | + type: article |
| 30 | + journal: 'Software: Practice and Experience' |
| 31 | + number: '6' |
| 32 | + volume: '51' |
| 33 | + pages: 1322-1351 |
| 34 | + year: 2021 |
| 35 | + month: 3 |
| 36 | + abstract: A significant aspect of designing new programming languages is to define |
| 37 | + their operational semantics. Working with a pen and paper version of such a semantics |
| 38 | + is notoriously difficult. For this reason, tools for computer aided semantics |
| 39 | + engineering were created. Many of these tools allow programmers to execute their |
| 40 | + language's operational semantics. An executable semantics makes it easier to verify |
| 41 | + whether the execution of a program leads to the desired result. When a program |
| 42 | + exhibits unexpected behavior, the programmer can consult the reduction graph to |
| 43 | + see what went wrong. Unfortunately, visualization of these graphs is currently |
| 44 | + not well-supported by most tools. Consequently, the comprehension of errors remains |
| 45 | + challenging. In this article, we present GraphRedex an open-source tool that empowers |
| 46 | + language designers to interactively explore their reduction graphs, offering three |
| 47 | + main benefits. First, a global exploration mode allows users to obtain a bird's-eye |
| 48 | + overview of the reduction graph and learn its high level workings. Second, a local |
| 49 | + exploration mode lets the programmer closely interact with the individual reduction |
| 50 | + rules. Third, our query interface allows the programmer to filter out and highlight |
| 51 | + specific regions of the reduction graph. We evaluated our tool by carrying out |
| 52 | + a user study showing that participants comprehend programs on average twice as |
| 53 | + fast while being able to answer questions more accurately. Finally, we demonstrate |
| 54 | + how GraphRedex helps to understand the semantics of two published works. Exploration |
| 55 | + of the semantics with GraphRedex unveiled an issue in one of the implementations |
| 56 | + of these works, which the author confirmed. |
| 57 | + keywords: |
| 58 | + - operational semantics |
| 59 | + - PLT Redex |
| 60 | + - semantics engineering |
| 61 | + - state explosion |
| 62 | + - tooling |
| 63 | + - visualization |
0 commit comments