Issue
DARTS, Volume 6, Issue 2
Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
-
Part of:
Volume:
DARTS, Volume 6 (ECOOP 2020)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2020-11-06
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts6
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{nguyenquangdo_et_al:DARTS.6.2.0,
author = {Nguyen Quang Do, Lisa and Rigger, Manuel},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Nguyen Quang Do, Lisa and Rigger, Manuel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.0},
URN = {urn:nbn:de:0030-drops-131977},
doi = {10.4230/DARTS.6.2.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
Flow-Sensitive Type-Based Heap Cloning (Artifact)
Abstract
This artifact contains our implementation of a new flow-sensitive type-based points-to analysis, described in "Flow-Sensitive Type-Based Heap Cloning" by Mohamad Barbar, Yulei Sui, and Shiping Chen (ECOOP 2020). This analysis performs heap cloning based on C and C++ types rather than calling contexts. Packaged as a Docker image, the artifact allows users to reproduce the claims made in the "Evaluation" section of the associated paper (Section 5.2) and to build and analyse arbitrary software.
Cite as
Mohamad Barbar, Yulei Sui, and Shiping Chen. Flow-Sensitive Type-Based Heap Cloning (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{barbar_et_al:DARTS.6.2.1,
author = {Barbar, Mohamad and Sui, Yulei and Chen, Shiping},
title = {{Flow-Sensitive Type-Based Heap Cloning (Artifact)}},
pages = {1:1--1:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Barbar, Mohamad and Sui, Yulei and Chen, Shiping},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.1},
URN = {urn:nbn:de:0030-drops-131988},
doi = {10.4230/DARTS.6.2.1},
annote = {Keywords: Heap cloning, type-based analysis, flow-sensitivity}
}
Document
Artifact
A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)
Abstract
Idris' Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, Resources allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.
Cite as
Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede. A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{demuijnckhughes_et_al:DARTS.6.2.2,
author = {de Muijnck-Hughes, Jan and Brady, Edwin and Vanderbauwhede, Wim},
title = {{A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)}},
pages = {2:1--2:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {de Muijnck-Hughes, Jan and Brady, Edwin and Vanderbauwhede, Wim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.2},
URN = {urn:nbn:de:0030-drops-131995},
doi = {10.4230/DARTS.6.2.2},
annote = {Keywords: Dependent Types, Algebraic Effect Handlers, Domain-Specific Languages, Embedded Domain Specific Languages, Idris, Substructural Type-Systems}
}
Document
Artifact
Putting Randomized Compiler Testing into Production (Artifact)
Abstract
This artifact accompanies our experience report for our compiler testing technology transfer project: taking the GraphicsFuzz research project on randomized metamorphic testing of graphics shader compilers, and building the necessary tooling around it to provide a highly automated process for improving the Khronos Vulkan Conformance Test Suite (CTS) with test cases that expose fuzzer-found compiler bugs, or that plug gaps in test coverage. The artifact consists of two Dockerfiles and associated files that can be used to build two Docker containers. The containers include our main tool for performing fuzzing: gfauto. The containers allow the user to fuzz SwiftShader, a software Vulkan implementation, finding 4 bugs. The user will also perform some line coverage analysis of SwiftShader using our tools to synthesize a small test that increases line coverage. Ubuntu, gfauto, SwiftShader, and other dependencies inside the Docker containers are fixed at specific versions, and all random seeds are set to specific values. Thus, all examples should reproduce faithfully on any machine.
Cite as
Alastair F. Donaldson, Hugues Evrard, and Paul Thomson. Putting Randomized Compiler Testing into Production (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{donaldson_et_al:DARTS.6.2.3,
author = {Donaldson, Alastair F. and Evrard, Hugues and Thomson, Paul},
title = {{Putting Randomized Compiler Testing into Production (Artifact)}},
pages = {3:1--3:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Donaldson, Alastair F. and Evrard, Hugues and Thomson, Paul},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.3},
URN = {urn:nbn:de:0030-drops-132005},
doi = {10.4230/DARTS.6.2.3},
annote = {Keywords: Compilers, metamorphic testing, 3D graphics, experience report}
}
Document
Artifact
Reconciling Event Structures with Modern Multiprocessors (Artifact)
Abstract
The artifact is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package imm contains a modified version of the Intermediate Memory Model, extended with the support of sequentially consistent atomics, and the compilation correctness proofs from it to hardware models. The second package weakestmoToImm contains a definition of the Weakestmo memory model as well as a compilation correctness proof from it to IMM.
Cite as
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{moiseenko_et_al:DARTS.6.2.4,
author = {Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
title = {{Reconciling Event Structures with Modern Multiprocessors (Artifact)}},
pages = {4:1--4:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.4},
URN = {urn:nbn:de:0030-drops-132015},
doi = {10.4230/DARTS.6.2.4},
annote = {Keywords: Weak Memory Consistency, Event Structures, IMM, Weakestmo}
}
Document
Artifact
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)
Abstract
This artifact contains the implementation of JaVerT.Click, a symbolic analysis tool for modern event-driven Web applications. The tool extends JaVerT 2.0, a state-of-the-art symbolic execution tool for JavaScript (JS), with JS reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations mostly follow the respective standards line-by-line and are all thoroughly tested against the official test suite. We also evaluate JaVerT.Click by performing symbolic analysis on two real-world libraries: cash and p-map, finding three previously unknown bugs.
Cite as
Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{sampaio_et_al:DARTS.6.2.5,
author = {Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
title = {{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)}},
pages = {5:1--5:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.5},
URN = {urn:nbn:de:0030-drops-132028},
doi = {10.4230/DARTS.6.2.5},
annote = {Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}
Document
Artifact
Static Analysis of Shape in TensorFlow Programs (Artifact)
Abstract
These instructions are intended for using the artifact for our ECOOP'20 paper entitled "Static Analysis of Shape in TensorFlow Programs". They can be used to run Pythia - the tool implementing the paper’s analysis - on the paper’s evaluation set demonstrating bug detection in the most precise configuration of our analysis as well as the precision of the analysis under different configurations.
Cite as
Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis. Static Analysis of Shape in TensorFlow Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 6:1-6:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{lagouvardos_et_al:DARTS.6.2.6,
author = {Lagouvardos, Sifis and Dolby, Julian and Grech, Neville and Antoniadis, Anastasios and Smaragdakis, Yannis},
title = {{Static Analysis of Shape in TensorFlow Programs (Artifact)}},
pages = {6:1--6:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Lagouvardos, Sifis and Dolby, Julian and Grech, Neville and Antoniadis, Anastasios and Smaragdakis, Yannis},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.6},
URN = {urn:nbn:de:0030-drops-132035},
doi = {10.4230/DARTS.6.2.6},
annote = {Keywords: Python, TensorFlow, static analysis, Doop, Wala}
}
Document
Artifact
Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model (Artifact)
Abstract
This artefact provides runnable versions of the code samples given in the main publication. An interpreter for the Stella language is provided together with a basic web-based IDE (syntax highlighting + running programs) which is able to run all Stella code given in the main publication. Also included are runnable implementations of the running example from the main publication (a simple wind turbine simulator) implemented in Stella and 6 other languages and frameworks (Akka, Flapjax, FrTime, ReactJS, REScala, and RxJS). While we do not discuss how these other technologies work, we highlight the interesting parts of the implementations of the running example: the difficulties we had, and any particular points of interest related to the claims made in the main publication.
Cite as
Sam Van den Vonder, Thierry Renaux, Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter. Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 7:1-7:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{vandenvonder_et_al:DARTS.6.2.7,
author = {Van den Vonder, Sam and Renaux, Thierry and Oeyen, Bjarno and De Koster, Joeri and De Meuter, Wolfgang},
title = {{Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model (Artifact)}},
pages = {7:1--7:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Van den Vonder, Sam and Renaux, Thierry and Oeyen, Bjarno and De Koster, Joeri and De Meuter, Wolfgang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.7},
URN = {urn:nbn:de:0030-drops-132045},
doi = {10.4230/DARTS.6.2.7},
annote = {Keywords: functional reactive programming, reactive programming, reactive streams, actors, reactors}
}
Document
Artifact
The Duality of Subtyping (Artifact)
Abstract
This artifact contains the Coq formalization associated with the paper The Duality of Subtyping submitted in ECOOP 2020. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Sections 1-7 explain the basic information about the artifact. Section A explains how to get the docker image for the artifact. Section B explains the prerequisites and the steps to run coq files from scratch. Section C explains coq files briefly. Section D shows the correspondence between important lemmas discussed in paper and their respective Coq formalization. The term MonoTyping used in artifact corresponds to the standard subtyping systems.
Cite as
Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman. The Duality of Subtyping (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 8:1-8:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{oliveira_et_al:DARTS.6.2.8,
author = {Oliveira, Bruno C. d. S. and Shaobo, Cui and Rehman, Baber},
title = {{The Duality of Subtyping (Artifact)}},
pages = {8:1--8:6},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Oliveira, Bruno C. d. S. and Shaobo, Cui and Rehman, Baber},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.8},
URN = {urn:nbn:de:0030-drops-132051},
doi = {10.4230/DARTS.6.2.8},
annote = {Keywords: DuoTyping, OOP, Duality, Subtyping, Supertyping}
}
Document
Artifact
A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)
Abstract
Our companion paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The artifact contains the specification of λ_i^{:} and its TDOS, and related Coq code. λ_i^{:} is formalized using the locally nameless representation with cofinite quantification. The Coq definition and some infrastructure code are generated by Ott and LNgen. λ_i^{:} is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016), and a simple variant of it is designed to demonstrate the possibility to match with them without any modification. To relate the two calculi with λ_i^{:}, a sound theorem on semantics and a completeness theorem on typing are proved for each variant. In addition, we extended the bidirectional typing of Oliveira et al.’s λ_i calculus, and designed an elaboration from it to λ_i^{:}, to show that many of λ_i^{:}’s explicit annotations can be inferred automatically.
Cite as
Xuejing Huang and Bruno C. d. S. Oliveira. A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 9:1-9:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{huang_et_al:DARTS.6.2.9,
author = {Huang, Xuejing and Oliveira, Bruno C. d. S.},
title = {{A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)}},
pages = {9:1--9:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Huang, Xuejing and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.9},
URN = {urn:nbn:de:0030-drops-132060},
doi = {10.4230/DARTS.6.2.9},
annote = {Keywords: operational semantics, type systems, intersection types}
}
Document
Artifact
Blame for Null (Artifact)
Abstract
This artifact is a companion to the paper "Blame for Null", where we formalize multiple calculi to reason about the interoperability between languages where nullability is explicit and those where nullability is implicit. Our main result is a theorem that states that nullability errors can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. We summarize our result with the slogan explicitly nullable programs can't be blamed. The artifact consists of a mechanized Coq proof of the results presented in the paper.
Cite as
Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{nieto_et_al:DARTS.6.2.10,
author = {Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
title = {{Blame for Null (Artifact)}},
pages = {10:1--10:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.10},
URN = {urn:nbn:de:0030-drops-132070},
doi = {10.4230/DARTS.6.2.10},
annote = {Keywords: nullability, type systems, blame calculus, gradual typing}
}
Document
Artifact
Static Type Analysis by Abstract Interpretation of Python Programs (Artifact)
Abstract
Python is an increasingly popular dynamic programming language, particularly used in the scientific community and well-known for its powerful and permissive high-level syntax. Our work aims at detecting statically and automatically type errors. As these type errors are exceptions that can be caught later on, we precisely track all exceptions (raised or caught). We designed a static analysis by abstract interpretation able to infer the possible types of variables, taking into account the full control-flow. It handles both typing paradigms used in Python, nominal and structural, supports Python’s object model, introspection operators allowing dynamic type testing, dynamic attribute addition, as well as exception handling. We present a flow- and context-sensitive analysis with special domains to support containers (such as lists) and infer type equalities (allowing it to express parametric polymorphism). The analysis is soundly derived by abstract interpretation from a concrete semantics of Python developed by Fromherz et al. Our analysis is designed in a modular way as a set of domains abstracting a concrete collecting semantics. It has been implemented into the MOPSA analysis framework, and leverages external type annotations from the Typeshed project to support the vast standard library. We show that it scales to benchmarks a few thousand lines long, and preliminary results show it is able to analyze a small real-life command-line utility called PathPicker. Compared to previous work, it is sound, while it keeps similar efficiency and precision.
Cite as
Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. Static Type Analysis by Abstract Interpretation of Python Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 11:1-11:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{monat_et_al:DARTS.6.2.11,
author = {Monat, Rapha\"{e}l and Ouadjaout, Abdelraouf and Min\'{e}, Antoine},
title = {{Static Type Analysis by Abstract Interpretation of Python Programs (Artifact)}},
pages = {11:1--11:6},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Monat, Rapha\"{e}l and Ouadjaout, Abdelraouf and Min\'{e}, Antoine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.11},
URN = {urn:nbn:de:0030-drops-132082},
doi = {10.4230/DARTS.6.2.11},
annote = {Keywords: Formal Methods, Static Analysis, Abstract Interpretation, Type Analysis, Dynamic Programming Language, Python Semantics}
}
Document
Artifact
Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)
Abstract
This artifact contains a version of the Godel tool that checks MiGo+ types - an extension of MiGo from [Lange et al., 2018] including GoL. Given the extracted MiGo+ types, the tool can analyse them using the mCRL2 model checker to check several properties including liveness, safety and data race freedom as defined in our paper. The artifact also includes examples, shipped with both the source of the Godel tool and the benchmark repository. The latter also contains the Go source for the benchmark examples. We provide compiled binaries of the artifact in a Docker image, with instructions on how to use them. Finally, for convenience, the Docker image also contains a binary version of the migoinfer+ tool, developed as a fork from the original migoinfer by Nicholas Ng in [Lange et al., 2018]. This new version adds the ability to extract shared memory pointers as well as Mutex and RWMutex locks.
Cite as
Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{gabet_et_al:DARTS.6.2.12,
author = {Gabet, Julia and Yoshida, Nobuko},
title = {{Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)}},
pages = {12:1--12:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Gabet, Julia and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.12},
URN = {urn:nbn:de:0030-drops-132096},
doi = {10.4230/DARTS.6.2.12},
annote = {Keywords: Go language, behavioural types, race detection, happens-before relation, safety, liveness}
}
Document
Artifact
Model-View-Update-Communicate: Session Types Meet the Elm Architecture (Artifact)
Abstract
Model-View-Update (MVU) is a development pattern for user interfaces pioneered by the Elm programming language. In the accompanying paper, we show a theoretical model of MVU, and detail how it can be extended to support session-typed communication.
This artifact consists of a Docker image which contains a version of the Links programming language, equipped with an MVU library supporting session-typed communication. The implementation is showcased by all examples provided in the paper, alongside larger examples including a two-factor authentication workflow and multi-room chat server.
Cite as
Simon Fowler. Model-View-Update-Communicate: Session Types Meet the Elm Architecture (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{fowler:DARTS.6.2.13,
author = {Fowler, Simon},
title = {{Model-View-Update-Communicate: Session Types Meet the Elm Architecture (Artifact)}},
pages = {13:1--13:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Fowler, Simon},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.13},
URN = {urn:nbn:de:0030-drops-132109},
doi = {10.4230/DARTS.6.2.13},
annote = {Keywords: Session types, concurrent programming, Model-View-Update}
}
Document
Artifact
Scala with Explicit Nulls (Artifact)
Abstract
This artifact is a companion to the paper "Scala with Explicit Nulls", where we present a modification to the Scala type system that makes nullability explicit in the types. Specifically, we make reference types non-nullable by default, while still allowing for nullable types via union types.
The artifact contains an implementation of this new type system design as a fork of the Dotty (Scala 3) compiler. Additionally, the artifact contains the source code of multiple Scala libraries that we used to evaluate our design.
Cite as
Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. Scala with Explicit Nulls (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{nieto_et_al:DARTS.6.2.14,
author = {Nieto, Abel and Zhao, Yaoyu and Lhot\'{a}k, Ond\v{r}ej and Chang, Angela and Pu, Justin},
title = {{Scala with Explicit Nulls (Artifact)}},
pages = {14:1--14:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Nieto, Abel and Zhao, Yaoyu and Lhot\'{a}k, Ond\v{r}ej and Chang, Angela and Pu, Justin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.14},
URN = {urn:nbn:de:0030-drops-132117},
doi = {10.4230/DARTS.6.2.14},
annote = {Keywords: Scala, Java, nullability, language interoperability, type systems}
}
Document
Artifact
Owicki-Gries Reasoning for C11 RAR (Artifact)
Abstract
The paper "Owicki-Gries Reasoning for C11 RAR" introduces a new proof calculus for the C11 RAR memory model that allows Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. The proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. The artifact includes the Isabelle formalisation of the proof method introduced in the paper. It also contains the formalisation and proof of all case studies presented in the paper. All of the theorems are accompanied with their respective proofs.
Cite as
Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{dalvandi_et_al:DARTS.6.2.15,
author = {Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
title = {{Owicki-Gries Reasoning for C11 RAR (Artifact)}},
pages = {15:1--15:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.15},
URN = {urn:nbn:de:0030-drops-132123},
doi = {10.4230/DARTS.6.2.15},
annote = {Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}
Document
Artifact
Perfect is the Enemy of Good: Best-Effort Program Synthesis (Artifact)
Abstract
Program synthesis promises to help software developers with everyday tasks by generating code snippets automatically from input-output examples and other high-level specifications. The conventional wisdom is that a synthesizer must always satisfy the specification exactly. We conjecture that this all-or-nothing paradigm stands in the way of adopting program synthesis as a developer tool: in practice, the user-written specification often contains errors or is simply too hard for the synthesizer to solve within a reasonable time; in these cases, the user is left with a single over-fitted result or, more often than not, no result at all. In this paper we propose a new program synthesis paradigm we call best-effort program synthesis, where the synthesizer returns a ranked list of partially-valid results, i.e., programs that satisfy some part of the specification.
To support this paradigm, we develop best-effort enumeration, a new synthesis algorithm that extends a popular program enumeration technique with the ability to accumulate and return multiple partially-valid results with minimal overhead. We implement this algorithm in a tool called BESTER, and evaluate it on 79 synthesis benchmarks from the literature. Contrary to the conventional wisdom, our evaluation shows that BESTER returns useful results even when the specification is flawed or too hard: i) for all benchmarks with an error in the specification, the top three BESTER results contain the correct solution, and ii) for most hard benchmarks, the top three results contain non-trivial fragments of the correct solution. We also performed an exploratory user study, which confirms our intuition that partially-valid results are useful: the study shows that programmers use the output of the synthesizer for comprehension and often incorporate it into their solutions.
Cite as
Hila Peleg and Nadia Polikarpova. Perfect is the Enemy of Good: Best-Effort Program Synthesis (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 16:1-16:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{peleg_et_al:DARTS.6.2.16,
author = {Peleg, Hila and Polikarpova, Nadia},
title = {{Perfect is the Enemy of Good: Best-Effort Program Synthesis (Artifact)}},
pages = {16:1--16:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Peleg, Hila and Polikarpova, Nadia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.16},
URN = {urn:nbn:de:0030-drops-132136},
doi = {10.4230/DARTS.6.2.16},
annote = {Keywords: Program Synthesis, Programming by Example}
}
Document
Artifact
Don't Panic! Better, Fewer, Syntax Errors for LR Parsers (Artifact)
Abstract
This is the artefact accompanying the paper "Don't Panic! Better, Fewer, Syntax Errors for LR Parsers" by Diekmann and Tratt. It focusses on the experiment from that paper, which compares a number of different error recovery algorithms on a large corpus of data, including all the software necessary to reproduce the experiment from the paper.
Cite as
Lukas Diekmann and Laurence Tratt. Don't Panic! Better, Fewer, Syntax Errors for LR Parsers (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 17:1-17:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{diekmann_et_al:DARTS.6.2.17,
author = {Diekmann, Lukas and Tratt, Laurence},
title = {{Don't Panic! Better, Fewer, Syntax Errors for LR Parsers (Artifact)}},
pages = {17:1--17:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Diekmann, Lukas and Tratt, Laurence},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.17},
URN = {urn:nbn:de:0030-drops-132143},
doi = {10.4230/DARTS.6.2.17},
annote = {Keywords: Parsing, error recovery, programming languages}
}
Document
Artifact
Multiparty Session Programming with Global Protocol Combinators (Artifact)
Abstract
In the paper "Multiparty Session Programming with Global Protocol Combinators", we introduce a library, ocaml-mpst for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. This artifact is the source code of ocaml-mpst, with all the examples and benchmarks discussed in the paper.
Cite as
Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming with Global Protocol Combinators (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{imai_et_al:DARTS.6.2.18,
author = {Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
title = {{Multiparty Session Programming with Global Protocol Combinators (Artifact)}},
pages = {18:1--18:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.18},
URN = {urn:nbn:de:0030-drops-132159},
doi = {10.4230/DARTS.6.2.18},
annote = {Keywords: Multiparty Session Types, Communication Protocol, Concurrent and Distributed Programming, OCaml}
}
Document
Artifact
Implementation of SHAPES Case Studies (Artifact)
Abstract
Our main paper presents {SHAPES}, a language extension which offers developers fine-grained control over the placement of data in memory, whilst retaining both memory safety and object abstraction via pooling and clustering. As part of the development of {SHAPES}, we wanted to investigate the usefulness of the concepts {SHAPES} brings to the table. To that extent, we implemented five such case studies. This publication provides the corresponding code and instructions on how to run these case studies and derive the results we provide.
Cite as
Alexandros Tasos, Juliana Franco, Sophia Drossopoulou, Tobias Wrigstad, and Susan Eisenbach. Implementation of SHAPES Case Studies (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 19:1-19:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Article{tasos_et_al:DARTS.6.2.19,
author = {Tasos, Alexandros and Franco, Juliana and Drossopoulou, Sophia and Wrigstad, Tobias and Eisenbach, Susan},
title = {{Implementation of SHAPES Case Studies (Artifact)}},
pages = {19:1--19:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
editor = {Tasos, Alexandros and Franco, Juliana and Drossopoulou, Sophia and Wrigstad, Tobias and Eisenbach, Susan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.19},
URN = {urn:nbn:de:0030-drops-132167},
doi = {10.4230/DARTS.6.2.19},
annote = {Keywords: Cache utilisation, Data representation, Memory safety}
}