10 Search Results for "Dolby, Julian"


Document
Symbolic Conflict Analysis in Pseudo-Boolean Optimization

Authors: Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)


Abstract
In the the last two decades, a lot of effort has been devoted to the development of satisfiability-checking tools for a variety of SAT-related problems. However, most of these tools lack optimization capabilities. That is, instead of finding any solution, one is sometimes interested in a solution that is best according to some criterion. Pseudo-Boolean solvers can be used to deal with optimization by successively solving a series of problems that contain an additional pseudo-Boolean constraint expressing that a better solution is required. A key point for the success of this simple approach is that lemmas that are learned for one problem can be reused for subsequent ones. In this paper we go one step further and show how, by using a simple symbolic conflict analysis procedure, not only can lemmas be reused between problems but also strengthened, thus further pruning the search space traversal. In addition, we show how this technique automatically allows one to infer upper bounds in maximization problems, thus giving an estimation of how far the solver is from finding an optimal solution. Experimental results with our PB solver reveal that (i) this technique is indeed effective in practice, providing important speedups in problems where several solutions are found and (ii) on problems with very few solutions, where the impact of our technique is limited, its overhead is negligible.

Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Symbolic Conflict Analysis in Pseudo-Boolean Optimization. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2025.23,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
  title =	{{Symbolic Conflict Analysis in Pseudo-Boolean Optimization}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.23},
  URN =		{urn:nbn:de:0030-drops-237579},
  doi =		{10.4230/LIPIcs.SAT.2025.23},
  annote =	{Keywords: SAT, Pseudo-Boolean Optimization, Conflict Analysis}
}
Document
Event Race Detection for Node.js Using Delay Injections

Authors: Andre Takeshi Endo and Anders Møller

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)


Abstract
Node.js is a widely used platform for building JavaScript server-side web applications, desktop applications, and software engineering tools. Its asynchronous execution model is essential for performance, but also gives rise to event races, which cause many subtle bugs that can be hard to detect and reproduce. Current solutions to expose such races are based on modifications of the source code of the Node.js system or on guided executions using complex happens-before modeling. This paper presents a simpler and more effective approach called NACD that works by dynamically instrumenting core asynchronous operations in the Node.js runtime system to inject delays and thereby reveal event race bugs. It consists of a small, robust runtime instrumentation module implemented in JavaScript that is configured by a flexible JSON model of the essential parts of the Node.js API. Experimental results show that NACD can reproduce event race bugs with higher probability and fewer runs than state-of-the-art tools.

Cite as

Andre Takeshi Endo and Anders Møller. Event Race Detection for Node.js Using Delay Injections. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 9:1-9:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{endo_et_al:LIPIcs.ECOOP.2025.9,
  author =	{Endo, Andre Takeshi and M{\o}ller, Anders},
  title =	{{Event Race Detection for Node.js  Using Delay Injections}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{9:1--9:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.9},
  URN =		{urn:nbn:de:0030-drops-233026},
  doi =		{10.4230/LIPIcs.ECOOP.2025.9},
  annote =	{Keywords: JavaScript, race conditions, flaky tests, event races, callback interleaving}
}
Document
Profile-Guided Field Externalization in an Ahead-Of-Time Compiler

Authors: Sebastian Kloibhofer, Lukas Makor, Peter Hofer, David Leopoldseder, and Hanspeter Mössenböck

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)


Abstract
Field externalization is a technique to reduce the footprint of objects by removing fields that most frequently contain zero or null. While researchers have developed ways to bring this optimization into the Java world, these have been limited to research compilers or virtual machines for embedded systems. In this work, we present a novel field externalization technique that uses information from static analysis and profiling to determine externalizable fields. During compilation, we remove those fields and define companion classes. These are used in case of non-default-value writes to the externalized fields. Our approach also correctly handles synchronization to prevent issues in multithreaded environments. We integrated our approach into the modern Java ahead-of-time compiler GraalVM Native Image. We conducted an evaluation on a diverse set of benchmarks that includes standard and microservice-based benchmarks. For standard benchmarks, our approach reduces the total allocated bytes by 2.76% and the maximum resident set size (max-RSS) by 2.55%. For microservice benchmarks, we achieved a reduction of 6.88% for normalized allocated bytes and 2.45% for max-RSS. We computed these improvements via the geometric mean. The median reductions are are 1.46% (alloc. bytes) and 0.22% (max-RSS) in standard benchmarks, as well as 3.63% (alloc. bytes) and 0.20% (max-RSS) in microservice benchmarks.

Cite as

Sebastian Kloibhofer, Lukas Makor, Peter Hofer, David Leopoldseder, and Hanspeter Mössenböck. Profile-Guided Field Externalization in an Ahead-Of-Time Compiler. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 19:1-19:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{kloibhofer_et_al:LIPIcs.ECOOP.2025.19,
  author =	{Kloibhofer, Sebastian and Makor, Lukas and Hofer, Peter and Leopoldseder, David and M\"{o}ssenb\"{o}ck, Hanspeter},
  title =	{{Profile-Guided Field Externalization in an Ahead-Of-Time Compiler}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{19:1--19:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.19},
  URN =		{urn:nbn:de:0030-drops-233121},
  doi =		{10.4230/LIPIcs.ECOOP.2025.19},
  annote =	{Keywords: compilation, instrumentation, profiling, fields, externalization, memory footprint reduction, memory footprint optimization}
}
Document
Practical Type-Based Taint Checking and Inference

Authors: Nima Karimipour, Kanak Das, Manu Sridharan, and Behnaz Hassanshahi

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)


Abstract
Many important security properties can be formulated in terms of flows of tainted data, and improved taint analysis tools to prevent such flows are of critical need. Most existing taint analyses use whole-program static analysis, leading to scalability challenges. Type-based checking is a promising alternative, as it enables modular and incremental checking for fast performance. However, type-based approaches have not been widely adopted in practice, due to challenges with false positives and annotating existing codebases. In this paper, we present a new approach to type-based checking of taint properties that addresses these challenges, based on two key techniques. First, we present a new type-based tainting checker with significantly reduced false positives, via more practical handling of third-party libraries and other language constructs. Second, we present a novel technique to automatically infer tainting type qualifiers for existing code. Our technique supports inference of generic type argument annotations, crucial for tainting properties. We implemented our techniques in a tool TaintTyper and evaluated it on real-world benchmarks. TaintTyper exceeds the recall of a state-of-the-art whole-program taint analyzer, with comparable precision, and 2.93X-22.9X faster checking time. Further, TaintTyper infers annotations comparable to those written by hand, suitable for insertion into source code. TaintTyper is a promising new approach to efficient and practical taint checking.

Cite as

Nima Karimipour, Kanak Das, Manu Sridharan, and Behnaz Hassanshahi. Practical Type-Based Taint Checking and Inference. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 18:1-18:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{karimipour_et_al:LIPIcs.ECOOP.2025.18,
  author =	{Karimipour, Nima and Das, Kanak and Sridharan, Manu and Hassanshahi, Behnaz},
  title =	{{Practical Type-Based Taint Checking and Inference}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{18:1--18:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.18},
  URN =		{urn:nbn:de:0030-drops-233119},
  doi =		{10.4230/LIPIcs.ECOOP.2025.18},
  annote =	{Keywords: Static analysis, Taint Analysis, Pluggable type systems, Security, Inference}
}
Document
PoTo: A Hybrid Andersen’s Points-To Analysis for Python

Authors: Ingkarat Rak-amnouykit, Ana Milanova, Guillaume Baudart, Martin Hirzel, and Julian Dolby

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)


Abstract
As Python is increasingly being adopted for large and complex programs, the importance of static analysis for Python (such as type inference) grows. Unfortunately, static analysis for Python remains a challenging task due to its dynamic language features and its abundant external libraries. To help fill this gap, this paper presents PoTo, an Andersen-style context-insensitive and flow-insensitive points-to analysis for Python. PoTo addresses Python-specific challenges and works for large programs via a novel hybrid evaluation, integrating traditional static points-to analysis with concrete evaluation in the Python interpreter for external library calls. We evaluate the analysis with two clients: type inference and call graph construction. This paper presents PoTo+, a static type inference for Python built on PoTo. We evaluate PoTo+ and compare it to two state-of-the-art Python type inference techniques: (1) the static rule-based Pytype and (2) the deep-learning based DLInfer. Our results show that PoTo+ outperforms both Pytype and DLInfer on existing Python packages. This paper also presents PoToCG, a call-graph construction analysis for Python built on PoTo. We compare PoToCG to PyCG, the state of the art for this problem, and show that PoTo produces more complete and more precise call graphs.

Cite as

Ingkarat Rak-amnouykit, Ana Milanova, Guillaume Baudart, Martin Hirzel, and Julian Dolby. PoTo: A Hybrid Andersen’s Points-To Analysis for Python. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 27:1-27:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{rakamnouykit_et_al:LIPIcs.ECOOP.2025.27,
  author =	{Rak-amnouykit, Ingkarat and Milanova, Ana and Baudart, Guillaume and Hirzel, Martin and Dolby, Julian},
  title =	{{PoTo: A Hybrid Andersen’s Points-To Analysis for Python}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{27:1--27:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.27},
  URN =		{urn:nbn:de:0030-drops-233194},
  doi =		{10.4230/LIPIcs.ECOOP.2025.27},
  annote =	{Keywords: Python, Points-to analysis, Machine learning libraries}
}
Document
Resource Paper
FAIR Jupyter: A Knowledge Graph Approach to Semantic Sharing and Granular Exploration of a Computational Notebook Reproducibility Dataset

Authors: Sheeba Samuel and Daniel Mietchen

Published in: TGDK, Volume 2, Issue 2 (2024): Special Issue on Resources for Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 2, Issue 2


Abstract
The way in which data are shared can affect their utility and reusability. Here, we demonstrate how data that we had previously shared in bulk can be mobilized further through a knowledge graph that allows for much more granular exploration and interrogation. The original dataset is about the computational reproducibility of GitHub-hosted Jupyter notebooks associated with biomedical publications. It contains rich metadata about the publications, associated GitHub repositories and Jupyter notebooks, and the notebooks' reproducibility. We took this dataset, converted it into semantic triples and loaded these into a triple store to create a knowledge graph - FAIR Jupyter - that we made accessible via a web service. This enables granular data exploration and analysis through queries that can be tailored to specific use cases. Such queries may provide details about any of the variables from the original dataset, highlight relationships between them or combine some of the graph’s content with materials from corresponding external resources. We provide a collection of example queries addressing a range of use cases in research and education. We also outline how sets of such queries can be used to profile specific content types, either individually or by class. We conclude by discussing how such a semantically enhanced sharing of complex datasets can both enhance their FAIRness - i.e., their findability, accessibility, interoperability, and reusability - and help identify and communicate best practices, particularly with regards to data quality, standardization, automation and reproducibility.

Cite as

Sheeba Samuel and Daniel Mietchen. FAIR Jupyter: A Knowledge Graph Approach to Semantic Sharing and Granular Exploration of a Computational Notebook Reproducibility Dataset. In Special Issue on Resources for Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 2, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Article{samuel_et_al:TGDK.2.2.4,
  author =	{Samuel, Sheeba and Mietchen, Daniel},
  title =	{{FAIR Jupyter: A Knowledge Graph Approach to Semantic Sharing and Granular Exploration of a Computational Notebook Reproducibility Dataset}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:24},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.2.4},
  URN =		{urn:nbn:de:0030-drops-225886},
  doi =		{10.4230/TGDK.2.2.4},
  annote =	{Keywords: Knowledge Graph, Computational reproducibility, Jupyter notebooks, FAIR data, PubMed Central, GitHub, Python, SPARQL}
}
Document
Artifact
Static Analysis of Shape in TensorFlow Programs (Artifact)

Authors: Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)


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
Static Analysis of Shape in TensorFlow Programs

Authors: Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
Machine learning has been widely adopted in diverse science and engineering domains, aided by reusable libraries and quick development patterns. The TensorFlow library is probably the best-known representative of this trend and most users employ the Python API to its powerful back-end. TensorFlow programs are susceptible to several systematic errors, especially in the dynamic typing setting of Python. We present Pythia, a static analysis that tracks the shapes of tensors across Python library calls and warns of several possible mismatches. The key technical aspects are a close modeling of library semantics with respect to tensor shape, and an identification of violations and error-prone patterns. Pythia is powerful enough to statically detect (with 84.62% precision) 11 of the 14 shape-related TensorFlow bugs in the recent Zhang et al. empirical study - an independent slice of real-world bugs.

Cite as

Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis. Static Analysis of Shape in TensorFlow Programs. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 15:1-15:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{lagouvardos_et_al:LIPIcs.ECOOP.2020.15,
  author =	{Lagouvardos, Sifis and Dolby, Julian and Grech, Neville and Antoniadis, Anastasios and Smaragdakis, Yannis},
  title =	{{Static Analysis of Shape in TensorFlow Programs}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{15:1--15:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.15},
  URN =		{urn:nbn:de:0030-drops-131726},
  doi =		{10.4230/LIPIcs.ECOOP.2020.15},
  annote =	{Keywords: Python, TensorFlow, static analysis, Doop, Wala}
}
Document
Tool Insights Paper
MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors (Tool Insights Paper)

Authors: Linghui Luo, Julian Dolby, and Eric Bodden

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
In the past, many static analyses have been created in academia, but only a few of them have found widespread use in industry. Those analyses which are adopted by developers usually have IDE support in the form of plugins, without which developers have no convenient mechanism to use the analysis. Hence, the key to making static analyses more accessible to developers is to integrate the analyses into IDEs and editors. However, integrating static analyses into IDEs is non-trivial: different IDEs have different UI workflows and APIs, expertise in those matters is required to write such plugins, and analysis experts are not typically familiar with doing this. As a result, especially in academia, most analysis tools are headless and only have command-line interfaces. To make static analyses more usable, we propose MagpieBridge - a general approach to integrating static analyses into IDEs and editors. MagpieBridge reduces the mxn complexity problem of integrating m analyses into n IDEs to m+n complexity because each analysis and type of plugin need be done just once for MagpieBridge itself. We demonstrate our approach by integrating two existing analyses, Ariadne and CogniCrypt, into IDEs; these two analyses illustrate the generality of MagpieBridge, as they are based on different program analysis frameworks - WALA and Soot respectively - for different application areas - machine learning and security - and different programming languages - Python and Java. We show further generality of MagpieBridge by using multiple popular IDEs and editors, such as Eclipse, IntelliJ, PyCharm, Jupyter, Sublime Text and even Emacs and Vim.

Cite as

Linghui Luo, Julian Dolby, and Eric Bodden. MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors (Tool Insights Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 21:1-21:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{luo_et_al:LIPIcs.ECOOP.2019.21,
  author =	{Luo, Linghui and Dolby, Julian and Bodden, Eric},
  title =	{{MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{21:1--21:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.21},
  URN =		{urn:nbn:de:0030-drops-108139},
  doi =		{10.4230/LIPIcs.ECOOP.2019.21},
  annote =	{Keywords: IDE, Tool Support, Static Analysis, Language Server Protocol}
}
Document
Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201)

Authors: Julian Dolby, Orna Grumberg, Peter Müller, and Omer Tripp

Published in: Dagstuhl Reports, Volume 6, Issue 5 (2016)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16201 "Synergies among Testing, Verification, and Repair for Concurrent Programs". This seminar builds upon, and is inspired by, several past seminars on program testing, verification, repair and combinations thereof. These include Dagstuhl Seminar 13021 "Symbolic Methods in Testing"; Dagstuhl Seminar 13061 "Fault Prediction, Localization and Repair"; Dagstuhl Seminar 14171 "Evaluating Software Verification Systems: Benchmarks and Competitions"; Dagstuhl Seminar 14352 "Next Generation Static Software Analysis Tools"; Dagstuhl Seminar 14442 "Symbolic Execution and Constraint Solving"; and Dagstuhl Seminar 15191 "Compositional Verification Methods for Next-Generation Concurrency". These were held in January 2013; February 2013; April 2014; August 2014; October 2014; and May 2015, respectively. Two notable contributions of Dagstuhl Seminar 16201, which distinguish it from these past seminars, are (i) the focus on concurrent programming, which introduces significant challenges to testing, verification and repair tools, as well as (ii) the goal of identifying and exploiting synergies between the testing, verification and repair research communities in light of common needs and goals.

Cite as

Julian Dolby, Orna Grumberg, Peter Müller, and Omer Tripp. Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). In Dagstuhl Reports, Volume 6, Issue 5, pp. 56-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{dolby_et_al:DagRep.6.5.56,
  author =	{Dolby, Julian and Grumberg, Orna and M\"{u}ller, Peter and Tripp, Omer},
  title =	{{Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201)}},
  pages =	{56--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{5},
  editor =	{Dolby, Julian and Grumberg, Orna and M\"{u}ller, Peter and Tripp, Omer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.5.56},
  URN =		{urn:nbn:de:0030-drops-67203},
  doi =		{10.4230/DagRep.6.5.56},
  annote =	{Keywords: (automatic) bug repair, concurrency bugs, concurrent programming, deductive verification, interactive verification, linearizability, synchronization testing}
}
  • Refine by Type
  • 10 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 5 2025
  • 1 2024
  • 2 2020
  • 1 2019
  • 1 2016

  • Refine by Author
  • 5 Dolby, Julian
  • 2 Antoniadis, Anastasios
  • 2 Grech, Neville
  • 2 Lagouvardos, Sifis
  • 2 Smaragdakis, Yannis
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 1 DARTS
  • 1 TGDK
  • 1 DagRep

  • Refine by Classification
  • 3 Software and its engineering → Compilers
  • 3 Software and its engineering → General programming languages
  • 2 Theory of computation → Program analysis
  • 1 Information systems → Entity relationship models
  • 1 Information systems → Information extraction
  • Show More...

  • Refine by Keyword
  • 4 Python
  • 2 Doop
  • 2 TensorFlow
  • 2 Wala
  • 2 static analysis
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail