51 Search Results for "Vitek, Jan"

Volume

LIPIcs, Volume 222

36th European Conference on Object-Oriented Programming (ECOOP 2022)

ECOOP 2022, June 6-10, 2022, Berlin, Germany

Editors: Karim Ali and Jan Vitek

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.27
The Fault in Our Stars: Designing Reproducible Large-scale Code Analysis Experiments

Authors: Petr Maj, Stefanie Muroya, Konrad Siek, Luca Di Grazia, and Jan Vitek

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Large-scale software repositories are a source of insights for software engineering. They offer an unmatched window into the software development process at scale. Their sheer number and size holds the promise of broadly applicable results. At the same time, that very size presents practical challenges for scaling tools and algorithms to millions of projects. A reasonable approach is to limit studies to representative samples of the population of interest. Broadly applicable conclusions can then be obtained by generalizing to the entire population. The contribution of this paper is a standardized experimental design methodology for choosing the inputs of studies working with large-scale repositories. We advocate for a methodology that clearly lays out what the population of interest is, how to sample it, and that fosters reproducibility. Along the way, we discourage researchers from using extrinsic attributes of projects such as stars, that measure some unclear notion of popularity.
Cite as

Petr Maj, Stefanie Muroya, Konrad Siek, Luca Di Grazia, and Jan Vitek. The Fault in Our Stars: Designing Reproducible Large-scale Code Analysis Experiments. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{maj_et_al:LIPIcs.ECOOP.2024.27,
  author =	{Maj, Petr and Muroya, Stefanie and Siek, Konrad and Di Grazia, Luca and Vitek, Jan},
  title =	{{The Fault in Our Stars: Designing Reproducible Large-scale Code Analysis Experiments}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.27},
  URN =		{urn:nbn:de:0030-drops-208769},
  doi =		{10.4230/LIPIcs.ECOOP.2024.27},
  annote =	{Keywords: software, mining code repositories, source code analysis}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ECOOP.2022
LIPIcs, Volume 222, ECOOP 2022, Complete Volume

Authors: Karim Ali and Jan Vitek

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
LIPIcs, Volume 222, ECOOP 2022, Complete Volume
Cite as

36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 1-940, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{ali_et_al:LIPIcs.ECOOP.2022,
  title =	{{LIPIcs, Volume 222, ECOOP 2022, Complete Volume}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{1--940},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022},
  URN =		{urn:nbn:de:0030-drops-162276},
  doi =		{10.4230/LIPIcs.ECOOP.2022},
  annote =	{Keywords: LIPIcs, Volume 222, ECOOP 2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ECOOP.2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Karim Ali and Jan Vitek

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ali_et_al:LIPIcs.ECOOP.2022.0,
  author =	{Ali, Karim and Vitek, Jan},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.0},
  URN =		{urn:nbn:de:0030-drops-162286},
  doi =		{10.4230/LIPIcs.ECOOP.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.1
Verified Compilation and Optimization of Floating-Point Programs in CakeML

Authors: Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
Cite as

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 1:1-1:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ECOOP.2022.1,
  author =	{Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
  title =	{{Verified Compilation and Optimization of Floating-Point Programs in CakeML}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{1:1--1:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.1},
  URN =		{urn:nbn:de:0030-drops-162290},
  doi =		{10.4230/LIPIcs.ECOOP.2022.1},
  annote =	{Keywords: compiler verification, compiler optimization, floating-point arithmetic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.2
Elementary Type Inference

Authors: Jinxu Zhao and Bruno C. d. S. Oliveira

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Languages with polymorphic type systems are made convenient to use by employing type inference to avoid redundant type information. Unfortunately, features such as impredicative types and subtyping make complete type inference very challenging or impossible to realize. This paper presents a form of partial type inference called elementary type inference. Elementary type inference adopts the idea of inferring only monotypes from past work on predicative higher-ranked polymorphism. This idea is extended with the addition of explicit type applications that work for any polytypes. Thus easy (predicative) instantiations can be inferred, while all other (impredicative) instantiations are always possible with explicit type applications without any compromise in expressiveness. Our target is a System F extension with top and bottom types, similar to the language employed by Pierce and Turner in their seminal work on local type inference. We show a sound, complete and decidable type system for a calculus called F_{< :}^e, that targets that extension of System F. A key design choice in F_{< :}^e is to consider top and bottom types as polytypes only. An important technical challenge is that the combination of predicative implicit instantiation and impredicative explicit type applications, in the presence of standard subtyping rules, is non-trivial. Without some restrictions, key properties, such as subsumption and stability of type substitution lemmas, break. To address this problem we introduce a variant of polymorphic subtyping called stable subtyping with some mild restrictions on implicit instantiation. All the results are mechanically formalized in the Abella theorem prover.
Cite as

Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{zhao_et_al:LIPIcs.ECOOP.2022.2,
  author =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  title =	{{Elementary Type Inference}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{2:1--2:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.2},
  URN =		{urn:nbn:de:0030-drops-162303},
  doi =		{10.4230/LIPIcs.ECOOP.2022.2},
  annote =	{Keywords: Type Inference}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.3
Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs

Authors: Madhurima Chakraborty, Renzo Olivares, Manu Sridharan, and Behnaz Hassanshahi

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Building sound and precise static call graphs for real-world JavaScript applications poses an enormous challenge, due to many hard-to-analyze language features. Further, the relative importance of these features may vary depending on the call graph algorithm being used and the class of applications being analyzed. In this paper, we present a technique to automatically quantify the relative importance of different root causes of call graph unsoundness for a set of target applications. The technique works by identifying the dynamic function data flows relevant to each call edge missed by the static analysis, correctly handling cases with multiple root causes and inter-dependent calls. We apply our approach to perform a detailed study of the recall of a state-of-the-art call graph construction technique on a set of framework-based web applications. The study yielded a number of useful insights. We found that while dynamic property accesses were the most common root cause of missed edges across the benchmarks, other root causes varied in importance depending on the benchmark, potentially useful information for an analysis designer. Further, with our approach, we could quickly identify and fix a recall issue in the call graph builder we studied, and also quickly assess whether a recent analysis technique for Node.js-based applications would be helpful for browser-based code. All of our code and data is publicly available, and many components of our technique can be re-used to facilitate future studies.
Cite as

Madhurima Chakraborty, Renzo Olivares, Manu Sridharan, and Behnaz Hassanshahi. Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 3:1-3:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.ECOOP.2022.3,
  author =	{Chakraborty, Madhurima and Olivares, Renzo and Sridharan, Manu and Hassanshahi, Behnaz},
  title =	{{Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{3:1--3:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.3},
  URN =		{urn:nbn:de:0030-drops-162314},
  doi =		{10.4230/LIPIcs.ECOOP.2022.3},
  annote =	{Keywords: JavaScript, call graph construction, static program analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.4
Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types

Authors: Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new typing discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).
Cite as

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lagaillardie_et_al:LIPIcs.ECOOP.2022.4,
  author =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  title =	{{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.4},
  URN =		{urn:nbn:de:0030-drops-162324},
  doi =		{10.4230/LIPIcs.ECOOP.2022.4},
  annote =	{Keywords: Rust language, affine multiparty session types, failures, cancellation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.5
How to Take the Inverse of a Type

Authors: Danielle Marshall and Dominic Orchard

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
In functional programming, regular types are a subset of algebraic data types formed from products and sums with their respective units. One can view regular types as forming a commutative semiring but where the usual axioms are isomorphisms rather than equalities. In this pearl, we show that regular types in a linear setting permit a useful notion of multiplicative inverse, allowing us to "divide" one type by another. Our adventure begins with an exploration of the properties and applications of this construction, visiting various topics from the literature including program calculation, Laurent polynomials, and derivatives of data types. Examples are given throughout using Haskell’s linear types extension to demonstrate the ideas. We then step through the looking glass to discover what might be possible in richer settings; the functional language Granule offers linear functions that incorporate local side effects, which allow us to demonstrate further algebraic structure. Lastly, we discuss whether dualities in linear logic might permit the related notion of an additive inverse.
Cite as

Danielle Marshall and Dominic Orchard. How to Take the Inverse of a Type. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 5:1-5:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{marshall_et_al:LIPIcs.ECOOP.2022.5,
  author =	{Marshall, Danielle and Orchard, Dominic},
  title =	{{How to Take the Inverse of a Type}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{5:1--5:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.5},
  URN =		{urn:nbn:de:0030-drops-162339},
  doi =		{10.4230/LIPIcs.ECOOP.2022.5},
  annote =	{Keywords: linear types, regular types, algebra of programming, derivatives}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.6
Compiling Volatile Correctly in Java

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 6:1-6:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ECOOP.2022.6,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{6:1--6:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.6},
  URN =		{urn:nbn:de:0030-drops-162346},
  doi =		{10.4230/LIPIcs.ECOOP.2022.6},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.7
Functional Programming with Datalog

Authors: André Pacak and Sebastian Erdweg

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Datalog is a carefully restricted logic programming language. What makes Datalog attractive is its declarative fixpoint semantics: Datalog queries consist of simple Horn clauses, yet Datalog solvers efficiently compute all derivable tuples even for recursive queries. However, as we argue in this paper, Datalog is ill-suited as a programming language and Datalog programs are hard to write and maintain. We propose a "new" frontend for Datalog: functional programming with sets called functional IncA. While programmers write recursive functions over algebraic data types and sets, we transparently translate all code to Datalog relations. However, we retain Datalog’s strengths: Functions that generate sets can encode arbitrary relations and mutually recursive functions have fixpoint semantics. We also ensure that the generated Datalog program terminates whenever the original functional program terminates, so that we can apply off-the-shelve bottom-up Datalog solvers. We demonstrate the versatility and ease of use of functional IncA by implementing a type checker, a program transformation, an interpreter of the untyped lambda calculus, two data-flow analyses, and clone detection of Java bytecode.
Cite as

André Pacak and Sebastian Erdweg. Functional Programming with Datalog. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 7:1-7:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{pacak_et_al:LIPIcs.ECOOP.2022.7,
  author =	{Pacak, Andr\'{e} and Erdweg, Sebastian},
  title =	{{Functional Programming with Datalog}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{7:1--7:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.7},
  URN =		{urn:nbn:de:0030-drops-162354},
  doi =		{10.4230/LIPIcs.ECOOP.2022.7},
  annote =	{Keywords: Datalog, functional programming, demand transformation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.8
Design-By-Contract for Flexible Multiparty Session Protocols

Authors: Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.
Cite as

Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-By-Contract for Flexible Multiparty Session Protocols. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 8:1-8:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gheri_et_al:LIPIcs.ECOOP.2022.8,
  author =	{Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
  title =	{{Design-By-Contract for Flexible Multiparty Session Protocols}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{8:1--8:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.8},
  URN =		{urn:nbn:de:0030-drops-162367},
  doi =		{10.4230/LIPIcs.ECOOP.2022.8},
  annote =	{Keywords: Choreography automata, design by contract, deadlock freedom, Communicating Finite State Machines, TypeScript programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.9
A Deterministic Memory Allocator for Dynamic Symbolic Execution

Authors: Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, and Cristian Cadar

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Dynamic symbolic execution (DSE) has established itself as an effective testing and analysis technique. While the memory model in DSE has attracted significant attention, the memory allocator has been largely ignored, despite its significant influence on DSE. In this paper, we discuss the different ways in which the memory allocator can influence DSE and the main design principles that a memory allocator for DSE needs to follow: support for external calls, cross-run and cross-path determinism, spatially and temporally distanced allocations, and stability. We then present KDAlloc, a deterministic allocator for DSE that is guided by these six design principles. We implement KDAlloc in KLEE, a popular DSE engine, and first show that it is competitive with KLEE’s default allocator in terms of performance and memory overhead, and in fact significantly improves performance in several cases. We then highlight its benefits for use-after-free error detection and two distinct DSE-based techniques: MoKlee, a system for saving DSE runs to disk and later (partially) restoring them, and SymLive, a system for finding infinite-loop bugs.
Cite as

Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, and Cristian Cadar. A Deterministic Memory Allocator for Dynamic Symbolic Execution. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schemmel_et_al:LIPIcs.ECOOP.2022.9,
  author =	{Schemmel, Daniel and B\"{u}ning, Julian and Busse, Frank and Nowack, Martin and Cadar, Cristian},
  title =	{{A Deterministic Memory Allocator for Dynamic Symbolic Execution}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{9:1--9:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.9},
  URN =		{urn:nbn:de:0030-drops-162372},
  doi =		{10.4230/LIPIcs.ECOOP.2022.9},
  annote =	{Keywords: memory allocation, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.10
Accumulation Analysis

Authors: Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
A typestate specification indicates which behaviors of an object are permitted in each of the object’s states. In the general case, soundly checking a typestate specification requires precise information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. This requirement has hindered the adoption of sound typestate analyses in practice. This paper identifies accumulation typestate specifications, which are the subset of typestate specifications that can be soundly checked without any information about aliasing. An accumulation typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow analysis that conservatively approximates the operations that have been performed on an object. This paper formalizes the notions of accumulation analysis and accumulation typestate specification. It proves that accumulation typestate specifications are exactly those typestate specifications that can be checked soundly without aliasing information. Further, 41% of the typestate specifications that appear in the research literature are accumulation typestate specifications.
Cite as

Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Accumulation Analysis. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 10:1-10:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kellogg_et_al:LIPIcs.ECOOP.2022.10,
  author =	{Kellogg, Martin and Shadab, Narges and Sridharan, Manu and Ernst, Michael D.},
  title =	{{Accumulation Analysis}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{10:1--10:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.10},
  URN =		{urn:nbn:de:0030-drops-162381},
  doi =		{10.4230/LIPIcs.ECOOP.2022.10},
  annote =	{Keywords: Typestate, finite-state property}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.11
Concolic Execution for WebAssembly

Authors: Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
WebAssembly (Wasm) is a new binary instruction format that allows targeted compiled code written in high-level languages to be executed by the browser’s JavaScript engine with near-native speed. Despite its clear performance advantages, Wasm opens up the opportunity for bugs or security vulnerabilities to be introduced into Web programs, as pre-existing issues in programs written in unsafe languages can be transferred down to cross-compiled binaries. The source code of such binaries is frequently unavailable for static analysis, creating the demand for tools that can directly tackle Wasm code. Despite this potentially security-critical situation, there is still a noticeable lack of tool support for analysing Wasm binaries. We present WASP, a symbolic execution engine for testing Wasm modules, which works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library for C and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; and was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.
Cite as

Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão. Concolic Execution for WebAssembly. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 11:1-11:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{marques_et_al:LIPIcs.ECOOP.2022.11,
  author =	{Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro},
  title =	{{Concolic Execution for WebAssembly}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{11:1--11:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.11},
  URN =		{urn:nbn:de:0030-drops-162394},
  doi =		{10.4230/LIPIcs.ECOOP.2022.11},
  annote =	{Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C Programs}
}
  • Refine by Author
  • 15 Vitek, Jan
  • 4 Chung, Benjamin
  • 3 Maj, Petr
  • 3 Oliveira, Bruno C. d. S.
  • 3 Zappa Nardelli, Francesco
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 Gradual typing
  • 3 concurrency
  • 3 type systems
  • 2 Concurrency
  • 2 Java
  • Show More...

  • Refine by Type
  • 50 document
  • 1 volume

  • Refine by Publication Year
  • 38 2022
  • 2 2015
  • 2 2017
  • 2 2018
  • 2 2019
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact