45 Search Results for "M�ller, Anders"

Document
DOI: 10.4230/OASIcs.ICPEC.2023.14
An Experience with and Reflections on Live Coding with Active Learning

Authors: Anders Schlichtkrull

Published in: OASIcs, Volume 112, 4th International Computer Programming Education Conference (ICPEC 2023)

Abstract
In this paper I report and reflect on a concrete experience with changing an introductory programming course from being based on "classical lectures" to being based on live coding with active learning. The experiment is built on learnings found in the literature and the pedagogical theories of scaffolding, think-pair-share and teaching as facilitation of learning. I reflect on the students' reaction to the experiment, the difficulty of the active learning, how to keep time, coverage of learning objectives, the degree of improvisation and student involvement. The experiment was well received by the students, and I report also on the feedback. My hope is that educators who want to introduce live coding with active learning will be able to draw inspiration from my preparation of, execution of and reflections on the experiment.
Cite as

Anders Schlichtkrull. An Experience with and Reflections on Live Coding with Active Learning. In 4th International Computer Programming Education Conference (ICPEC 2023). Open Access Series in Informatics (OASIcs), Volume 112, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{schlichtkrull:OASIcs.ICPEC.2023.14,
  author =	{Schlichtkrull, Anders},
  title =	{{An Experience with and Reflections on Live Coding with Active Learning}},
  booktitle =	{4th International Computer Programming Education Conference (ICPEC 2023)},
  pages =	{14:1--14:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-290-7},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{112},
  editor =	{Peixoto de Queir\'{o}s, Ricardo Alexandre and Teixeira Pinto, M\'{a}rio Paulo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2023.14},
  URN =		{urn:nbn:de:0030-drops-185108},
  doi =		{10.4230/OASIcs.ICPEC.2023.14},
  annote =	{Keywords: Live coding, active learning, teaching programming}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.14
A Univalent Formalization of Constructive Affine Schemes

Authors: Max Zeuner and Anders Mörtberg

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne’s classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.
Cite as

Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
  author =	{Zeuner, Max and M\"{o}rtberg, Anders},
  title =	{{A Univalent Formalization of Constructive Affine Schemes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{14:1--14:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14},
  URN =		{urn:nbn:de:0030-drops-184574},
  doi =		{10.4230/LIPIcs.TYPES.2022.14},
  annote =	{Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2023.6
Optimal Decremental Connectivity in Non-Sparse Graphs

Authors: Anders Aamand, Adam Karczmarz, Jakub Łącki, Nikos Parotsidis, Peter M. R. Rasmussen, and Mikkel Thorup

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We present a dynamic algorithm for maintaining the connected and 2-edge-connected components in an undirected graph subject to edge deletions. The algorithm is Monte-Carlo randomized and processes any sequence of edge deletions in O(m + n poly log n) total time. Interspersed with the deletions, it can answer queries whether any two given vertices currently belong to the same (2-edge-)connected component in constant time. Our result is based on a general Monte-Carlo randomized reduction from decremental c-edge-connectivity to a variant of fully-dynamic c-edge-connectivity on a sparse graph. For non-sparse graphs with Ω(n poly log n) edges, our connectivity and 2-edge-connectivity algorithms handle all deletions in optimal linear total time, using existing algorithms for the respective fully-dynamic problems. This improves upon an O(m log (n² / m) + n poly log n)-time algorithm of Thorup [J.Alg. 1999], which runs in linear time only for graphs with Ω(n²) edges. Our constant amortized cost for edge deletions in decremental connectivity in non-sparse graphs should be contrasted with an Ω(log n/log log n) worst-case time lower bound in the decremental setting [Alstrup, Husfeldt, and Rauhe FOCS'98] as well as an Ω(log n) amortized time lower-bound in the fully-dynamic setting [Patrascu and Demaine STOC'04].
Cite as

Anders Aamand, Adam Karczmarz, Jakub Łącki, Nikos Parotsidis, Peter M. R. Rasmussen, and Mikkel Thorup. Optimal Decremental Connectivity in Non-Sparse Graphs. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{aamand_et_al:LIPIcs.ICALP.2023.6,
  author =	{Aamand, Anders and Karczmarz, Adam and {\L}\k{a}cki, Jakub and Parotsidis, Nikos and Rasmussen, Peter M. R. and Thorup, Mikkel},
  title =	{{Optimal Decremental Connectivity in Non-Sparse Graphs}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.6},
  URN =		{urn:nbn:de:0030-drops-180581},
  doi =		{10.4230/LIPIcs.ICALP.2023.6},
  annote =	{Keywords: decremental connectivity, dynamic connectivity}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2022.1
Tiling with Squares and Packing Dominos in Polynomial Time

Authors: Anders Aamand, Mikkel Abrahamsen, Thomas Ahle, and Peter M. R. Rasmussen

Published in: LIPIcs, Volume 224, 38th International Symposium on Computational Geometry (SoCG 2022)

Abstract
A polyomino is a polygonal region with axis-parallel edges and corners of integral coordinates, which may have holes. In this paper, we consider planar tiling and packing problems with polyomino pieces and a polyomino container P. We give polynomial-time algorithms for deciding if P can be tiled with k× k squares for any fixed k which can be part of the input (that is, deciding if P is the union of a set of non-overlapping k× k squares) and for packing P with a maximum number of non-overlapping and axis-parallel 2× 1 dominos, allowing rotations by 90^∘. As packing is more general than tiling, the latter algorithm can also be used to decide if P can be tiled by 2× 1 dominos. These are classical problems with important applications in VLSI design, and the related problem of finding a maximum packing of 2× 2 squares is known to be NP-hard [J. Algorithms 1990]. For our three problems there are known pseudo-polynomial-time algorithms, that is, algorithms with running times polynomial in the area or perimeter of P. However, the standard, compact way to represent a polygon is by listing the coordinates of the corners in binary. We use this representation, and thus present the first polynomial-time algorithms for the problems. Concretely, we give a simple O(nlog n)-time algorithm for tiling with squares, where n is the number of corners of P. We then give a more involved algorithm that reduces the problems of packing and tiling with dominos to finding a maximum and perfect matching in a graph with O(n³) vertices. This leads to algorithms with running times O(n³(log³ n)/(log²log n)) and O(n³(log² n)/(log log n)), respectively.
Cite as

Anders Aamand, Mikkel Abrahamsen, Thomas Ahle, and Peter M. R. Rasmussen. Tiling with Squares and Packing Dominos in Polynomial Time. In 38th International Symposium on Computational Geometry (SoCG 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 224, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aamand_et_al:LIPIcs.SoCG.2022.1,
  author =	{Aamand, Anders and Abrahamsen, Mikkel and Ahle, Thomas and Rasmussen, Peter M. R.},
  title =	{{Tiling with Squares and Packing Dominos in Polynomial Time}},
  booktitle =	{38th International Symposium on Computational Geometry (SoCG 2022)},
  pages =	{1:1--1:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-227-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{224},
  editor =	{Goaoc, Xavier and Kerber, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2022.1},
  URN =		{urn:nbn:de:0030-drops-160096},
  doi =		{10.4230/LIPIcs.SoCG.2022.1},
  annote =	{Keywords: packing, tiling, polyominos}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.11
Synthetic Integral Cohomology in Cubical Agda

Authors: Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables significant simplifications of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new definition of the group structure for cohomology with ℤ-coefficients, optimized for efficient computations. We also invent an optimized definition of the cup product which allows us to give the first complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.
Cite as

Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic Integral Cohomology in Cubical Agda. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brunerie_et_al:LIPIcs.CSL.2022.11,
  author =	{Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
  title =	{{Synthetic Integral Cohomology in Cubical Agda}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.11},
  URN =		{urn:nbn:de:0030-drops-157310},
  doi =		{10.4230/LIPIcs.CSL.2022.11},
  annote =	{Keywords: Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ECOOP.2021
LIPIcs, Volume 194, ECOOP 2021, Complete Volume

Authors: Anders Møller and Manu Sridharan

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
LIPIcs, Volume 194, ECOOP 2021, Complete Volume
Cite as

35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 1-628, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{mller_et_al:LIPIcs.ECOOP.2021,
  title =	{{LIPIcs, Volume 194, ECOOP 2021, Complete Volume}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{1--628},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021},
  URN =		{urn:nbn:de:0030-drops-140422},
  doi =		{10.4230/LIPIcs.ECOOP.2021},
  annote =	{Keywords: LIPIcs, Volume 194, ECOOP 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ECOOP.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Anders Møller and Manu Sridharan

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

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

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

Copy BibTex To Clipboard

@InProceedings{mller_et_al:LIPIcs.ECOOP.2021.0,
  author =	{M{\o}ller, Anders and Sridharan, Manu},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{0:i--0:xxiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.0},
  URN =		{urn:nbn:de:0030-drops-140438},
  doi =		{10.4230/LIPIcs.ECOOP.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.1
Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers

Authors: Hendrik van Antwerpen and Eelco Visser

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Compilers that can type check compilation units in parallel can make more efficient use of multi-core architectures, which are nowadays widespread. Developing parallel type checker implementations is complicated by the need to handle concurrency and synchronization of parallel compilation units. Dependencies between compilation units are induced by name resolution, and a parallel type checker needs to ensure that units have defined all relevant names before other units do a lookup. Mutually recursive references and implicitly discovered dependencies between compilation units preclude determining a static compilation order for many programming languages. In this paper, we present a new framework for implementing hierarchical type checkers that provides implicit parallel execution in the presence of dynamic and mutual dependencies between compilation units. The resulting type checkers can be written without explicit handling of communication or synchronization between different compilation units. We achieve this by providing type checkers with an API for name resolution based on scope graphs, a language-independent formalism that supports a wide range of binding patterns. We introduce the notion of scope state to ensure safe name resolution. Scope state tracks the completeness of a scope, and is used to decide whether a scope graph query between compilation units must be delayed. Our framework is implemented in Java using the actor paradigm. We evaluated our approach by parallelizing the solver for Statix, a meta-language for type checkers based on scope graphs, using our framework. This parallelizes every Statix-based type checker, provided its specification follows a split declaration-type style. Benchmarks show that the approach results in speedups for the parallel Statix solver of up to 5.0x on 8 cores for real-world code bases.
Cite as

Hendrik van Antwerpen and Eelco Visser. Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 1:1-1:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{vanantwerpen_et_al:LIPIcs.ECOOP.2021.1,
  author =	{van Antwerpen, Hendrik and Visser, Eelco},
  title =	{{Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{1:1--1:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.1},
  URN =		{urn:nbn:de:0030-drops-140441},
  doi =		{10.4230/LIPIcs.ECOOP.2021.1},
  annote =	{Keywords: type checking, name resolution, parallel algorithms}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.2
Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow Analysis

Authors: Philipp Dominik Schubert, Ben Hermann, and Eric Bodden

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Static analysis is used to automatically detect bugs and security breaches, and aids compiler optimization. Whole-program analysis (WPA) can yield high precision, however causes long analysis times and thus does not match common software-development workflows, making it often impractical to use for large, real-world applications. This paper thus presents the design and implementation of ModAlyzer, a novel static-analysis approach that aims at accelerating whole-program analysis by making the analysis modular and compositional. It shows how to compute lossless, persisted summaries for callgraph, points-to and data-flow information, and it reports under which circumstances this function-level compositional analysis outperforms WPA. We implemented ModAlyzer as an extension to LLVM and PhASAR, and applied it to 12 real-world C and C++ applications. At analysis time, ModAlyzer modularly and losslessly summarizes the analysis effect of the library code those applications share, hence avoiding its repeated re-analysis. The experimental results show that the reuse of these summaries can save, on average, 72% of analysis time over WPA. Moreover, because it is lossless, the module-wise analysis fully retains precision and recall. Surprisingly, as our results show, it sometimes even yields precision superior to WPA. The initial summary generation, on average, takes about 3.67 times as long as WPA.
Cite as

Philipp Dominik Schubert, Ben Hermann, and Eric Bodden. Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow Analysis. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 2:1-2:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{schubert_et_al:LIPIcs.ECOOP.2021.2,
  author =	{Schubert, Philipp Dominik and Hermann, Ben and Bodden, Eric},
  title =	{{Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow Analysis}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{2:1--2:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.2},
  URN =		{urn:nbn:de:0030-drops-140453},
  doi =		{10.4230/LIPIcs.ECOOP.2021.2},
  annote =	{Keywords: Inter-procedural static analysis, compositional analysis, LLVM, C/C++}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.3
Gradual Program Analysis for Null Pointers

Authors: Sam Estep, Jenna Wise, Jonathan Aldrich, Éric Tanter, Johannes Bader, and Joshua Sunshine

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete annotations, many analysis tools are either too conservative, yielding false positives, or too optimistic, resulting in unsound analysis results. In order to flexibly and soundly deal with partially-annotated programs, we propose to build upon and adapt the gradual typing approach to abstract-interpretation-based program analyses. Specifically, we focus on null-pointer analysis and demonstrate that a gradual null-pointer analysis hits a sweet spot, by gracefully applying static analysis where possible and relying on dynamic checks where necessary for soundness. In addition to formalizing a gradual null-pointer analysis for a core imperative language, we build a prototype using the Infer static analysis framework, and present preliminary evidence that the gradual null-pointer analysis reduces false positives compared to two existing null-pointer checkers for Infer. Further, we discuss ways in which the gradualization approach used to derive the gradual analysis from its static counterpart can be extended to support more domains. This work thus provides a basis for future analysis tools that can smoothly navigate the tradeoff between human effort and run-time overhead to reduce the number of reported false positives.
Cite as

Sam Estep, Jenna Wise, Jonathan Aldrich, Éric Tanter, Johannes Bader, and Joshua Sunshine. Gradual Program Analysis for Null Pointers. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{estep_et_al:LIPIcs.ECOOP.2021.3,
  author =	{Estep, Sam and Wise, Jenna and Aldrich, Jonathan and Tanter, \'{E}ric and Bader, Johannes and Sunshine, Joshua},
  title =	{{Gradual Program Analysis for Null Pointers}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{3:1--3:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.3},
  URN =		{urn:nbn:de:0030-drops-140469},
  doi =		{10.4230/LIPIcs.ECOOP.2021.3},
  annote =	{Keywords: gradual typing, gradual verification, dataflow analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.4
Covariant Conversions (CoCo): A Design Pattern for Type-Safe Modular Software Evolution in Object-Oriented Systems

Authors: Jan Bessai, George T. Heineman, and Boris Düdder

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Software evolution is an essential challenge for all software engineers, typically addressed solely using code versioning systems and language-specific code analysis tools. Most versioning systems view the evolution of a system as a directed acyclic graph of steps, with independent branches that could be merged. What these systems fail to provide is the ability to ensure stable APIs or that each subsequent evolution represents a cohesive extension yielding a valid system. Modular software evolution ensures that APIs remain stable, which is achieved by ensuring that only additional methods, fields, and data types are added, while treating existing modules through blackbox interfaces. Even with these restrictions, it must be possible to add new variations, fields, and methods without extensive duplication of prior module code. In contrast to most literature, our focus is on ensuring modular software evolution using mainstream object-oriented programming languages, instead of resorting to novel language extensions. We present a novel CoCo design pattern that supports type-safe covariantly overridden convert methods to transform earlier data type instances into their newest evolutionary representation to access operations that had been added later. CoCo supports both binary methods and producer methods. We validate and contrast our approach using a well-known compiler construction case study that other researchers have also investigated for modular evolution. Our resulting implementation relies on less boilerplate code, is completely type-safe, and allows clients to use normal object-oriented calling conventions. We also compare CoCo with existing approaches to the Expression Problem. We conclude by discussing how CoCo could change the direction of currently proposed Java language extensions to support closed-world assumptions about data types, as borrowed from functional programming.
Cite as

Jan Bessai, George T. Heineman, and Boris Düdder. Covariant Conversions (CoCo): A Design Pattern for Type-Safe Modular Software Evolution in Object-Oriented Systems. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 4:1-4:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bessai_et_al:LIPIcs.ECOOP.2021.4,
  author =	{Bessai, Jan and Heineman, George T. and D\"{u}dder, Boris},
  title =	{{Covariant Conversions (CoCo): A Design Pattern for Type-Safe Modular Software Evolution in Object-Oriented Systems}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{4:1--4:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.4},
  URN =		{urn:nbn:de:0030-drops-140476},
  doi =		{10.4230/LIPIcs.ECOOP.2021.4},
  annote =	{Keywords: Expression problem, software evolution, type safety, producer method, binary method}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.5
ALPACAS: A Language for Parametric Assessment of Critical Architecture Safety

Authors: Maxime Buyse, Rémi Delmas, and Youssef Hamadi

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
This paper introduces Alpacas, a domain-specific language and algorithms aimed at architecture modeling and safety assessment for critical systems. It allows to study the effects of random and systematic faults on complex critical systems and their reliability. The underlying semantic framework of the language is Stochastic Guarded Transition Systems, for which Alpacas provides a feature-rich declarative modeling language and algorithms for symbolic analysis and Monte-Carlo simulation, allowing to compute safety indicators such as minimal cutsets and reliability. Built as a domain-specific language deeply embedded in Scala 3, Alpacas offers generic modeling capabilities and type-safety unparalleled in other existing safety assessment frameworks. This improved expressive power allows to address complex system modeling tasks, such as formalizing the architectural design space of a critical function, and exploring it to identify the most reliable variant. The features and algorithms of Alpacas are illustrated on a case study of a thrust allocation and power dispatch system for an electric vertical takeoff and landing aircraft.
Cite as

Maxime Buyse, Rémi Delmas, and Youssef Hamadi. ALPACAS: A Language for Parametric Assessment of Critical Architecture Safety. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 5:1-5:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{buyse_et_al:LIPIcs.ECOOP.2021.5,
  author =	{Buyse, Maxime and Delmas, R\'{e}mi and Hamadi, Youssef},
  title =	{{ALPACAS: A Language for Parametric Assessment of Critical Architecture Safety}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{5:1--5:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.5},
  URN =		{urn:nbn:de:0030-drops-140487},
  doi =		{10.4230/LIPIcs.ECOOP.2021.5},
  annote =	{Keywords: Domain-Specific Language, Deep Embedding, Scala 3, Architecture Modelling, Safety Assessment, Static Analysis, Monte-Carlo Methods}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.6
CodeDJ: Reproducible Queries over Large-Scale Software Repositories

Authors: Petr Maj, Konrad Siek, Alexander Kovalenko, and Jan Vitek

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Analyzing massive code bases is a staple of modern software engineering research – a welcome side-effect of the advent of large-scale software repositories such as GitHub. Selecting which projects one should analyze is a labor-intensive process, and a process that can lead to biased results if the selection is not representative of the population of interest. One issue faced by researchers is that the interface exposed by software repositories only allows the most basic of queries. CodeDJ is an infrastructure for querying repositories composed of a persistent datastore, constantly updated with data acquired from GitHub, and an in-memory database with a Rust query interface. CodeDJ supports reproducibility, historical queries are answered deterministically using past states of the datastore; thus researchers can reproduce published results. To illustrate the benefits of CodeDJ, we identify biases in the data of a published study and, by repeating the analysis with new data, we demonstrate that the study’s conclusions were sensitive to the choice of projects.
Cite as

Petr Maj, Konrad Siek, Alexander Kovalenko, and Jan Vitek. CodeDJ: Reproducible Queries over Large-Scale Software Repositories. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 6:1-6:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{maj_et_al:LIPIcs.ECOOP.2021.6,
  author =	{Maj, Petr and Siek, Konrad and Kovalenko, Alexander and Vitek, Jan},
  title =	{{CodeDJ: Reproducible Queries over Large-Scale Software Repositories}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{6:1--6:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.6},
  URN =		{urn:nbn:de:0030-drops-140498},
  doi =		{10.4230/LIPIcs.ECOOP.2021.6},
  annote =	{Keywords: Software, Mining Code Repositories, Source Code Analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.7
Enabling Additional Parallelism in Asynchronous JavaScript Applications

Authors: Ellen Arteca, Frank Tip, and Max Schäfer

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
JavaScript is a single-threaded programming language, so asynchronous programming is practiced out of necessity to ensure that applications remain responsive in the presence of user input or interactions with file systems and networks. However, many JavaScript applications execute in environments that do exhibit concurrency by, e.g., interacting with multiple or concurrent servers, or by using file systems managed by operating systems that support concurrent I/O. In this paper, we demonstrate that JavaScript programmers often schedule asynchronous I/O operations suboptimally, and that reordering such operations may yield significant performance benefits. Concretely, we define a static side-effect analysis that can be used to determine how asynchronous I/O operations can be refactored so that asynchronous I/O-related requests are made as early as possible, and so that the results of these requests are awaited as late as possible. While our static analysis is potentially unsound, we have not encountered any situations where it suggested reorderings that change program behavior. We evaluate the refactoring on 20 applications that perform file- or network-related I/O. For these applications, we observe average speedups ranging between 0.99% and 53.6% for the tests that execute refactored code (8.1% on average).
Cite as

Ellen Arteca, Frank Tip, and Max Schäfer. Enabling Additional Parallelism in Asynchronous JavaScript Applications. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 7:1-7:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{arteca_et_al:LIPIcs.ECOOP.2021.7,
  author =	{Arteca, Ellen and Tip, Frank and Sch\"{a}fer, Max},
  title =	{{Enabling Additional Parallelism in Asynchronous JavaScript Applications}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{7:1--7:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.7},
  URN =		{urn:nbn:de:0030-drops-140501},
  doi =		{10.4230/LIPIcs.ECOOP.2021.7},
  annote =	{Keywords: asynchronous programming, refactoring, side-effect analysis, performance optimization, static analysis, JavaScript}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.8
Differential Privacy for Coverage Analysis of Software Traces

Authors: Yu Hao, Sufian Latif, Hailong Zhang, Raef Bassily, and Atanas Rountev

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
This work considers software execution traces, where a trace is a sequence of run-time events. Each user of a software system collects the set of traces covered by her execution of the software, and reports this set to an analysis server. Our goal is to report the local data of each user in a privacy-preserving manner by employing local differential privacy, a powerful theoretical framework for designing privacy-preserving data analysis. A significant advantage of such analysis is that it offers principled "built-in" privacy with clearly-defined and quantifiable privacy protections. In local differential privacy, the data of an individual user is modified using a local randomizer before being sent to the untrusted analysis server. Based on the randomized information from all users, the analysis server computes, for each trace, an estimate of how many users have covered it. Such analysis requires that the domain of possible traces be defined ahead of time. Unlike in prior related work, here the domain is either infinite or, at best, restricted to many billions of elements. Further, the traces in this domain typically have structure defined by the static properties of the software. To capture these novel aspects, we define the trace domain with the help of context-free grammars. We illustrate this approach with two exemplars: a call chain analysis in which traces are described through a regular language, and an enter/exit trace analysis in which traces are described by a balanced-parentheses context-free language. Randomization over such domains is challenging due to their large size, which makes it impossible to use prior randomization techniques. To solve this problem, we propose to use count sketch, a fixed-size hashing data structure for summarizing frequent items. We develop a version of count sketch for trace analysis and demonstrate its suitability for software execution data. In addition, instead of randomizing separately each contribution to the sketch, we develop a much-faster one-shot randomization of the accumulated sketch data. One important client of the collected information is the identification of high-frequency ("hot") traces. We develop a novel approach to identify hot traces from the collected randomized sketches. A key insight is that the very large domain of possible traces can be efficiently explored for hot traces by using the frequency estimates of a visited trace and its prefixes and suffixes. Our experimental study of both call chain analysis and enter/exit trace analysis indicates that the frequency estimates, as well as the identification of hot traces, achieve high accuracy and high privacy.
Cite as

Yu Hao, Sufian Latif, Hailong Zhang, Raef Bassily, and Atanas Rountev. Differential Privacy for Coverage Analysis of Software Traces. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 8:1-8:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hao_et_al:LIPIcs.ECOOP.2021.8,
  author =	{Hao, Yu and Latif, Sufian and Zhang, Hailong and Bassily, Raef and Rountev, Atanas},
  title =	{{Differential Privacy for Coverage Analysis of Software Traces}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{8:1--8:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.8},
  URN =		{urn:nbn:de:0030-drops-140513},
  doi =		{10.4230/LIPIcs.ECOOP.2021.8},
  annote =	{Keywords: Trace Profiling, Differential Privacy, Program Analysis}
}
  • Refine by Author
  • 5 Møller, Anders
  • 4 Mörtberg, Anders
  • 3 Aamand, Anders
  • 3 Gutin, Gregory
  • 3 Yeo, Anders
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Type theory
  • 3 Software and its engineering
  • 3 Software and its engineering → Concurrent programming languages
  • 3 Software and its engineering → Object oriented languages
  • 3 Theory of computation → Constructive mathematics
  • Show More...

  • Refine by Keyword
  • 4 JavaScript
  • 2 Coq
  • 2 Cubical Agda
  • 2 Preface
  • 2 Table of Contents
  • Show More...

  • Refine by Type
  • 45 document

  • Refine by Publication Year
  • 24 2021
  • 7 2013
  • 4 2018
  • 3 2020
  • 3 2023
  • 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 Imprint Privacy Contact