DROPS

Document

Testing Program Analyzers and Verifiers (Dagstuhl Seminar 25242)

Authors: Maria Christakis, Alastair F. Donaldson, John Regehr, and Thodoris Sotiropoulos

Published in: Dagstuhl Reports, Volume 15, Issue 6 (2026)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 25242 "Testing Program Analyzers and Verifiers". Program analyzers and verifiers are routinely employed during software development to prevent and detect faults. In this seminar, we examine the impact of faults within these tools, distinguishing between those that are critical and those that are less severe. We also explore and discuss state-of-the-art techniques for uncovering faults in program analyzers and verifiers, their connections to related domains such as compiler testing, and potential future directions for improving their reliability.

Cite as

Maria Christakis, Alastair F. Donaldson, John Regehr, and Thodoris Sotiropoulos. Testing Program Analyzers and Verifiers (Dagstuhl Seminar 25242). In Dagstuhl Reports, Volume 15, Issue 6, pp. 69-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{christakis_et_al:DagRep.15.6.69,
  author =	{Christakis, Maria and Donaldson, Alastair F. and Regehr, John and Sotiropoulos, Thodoris},
  title =	{{Testing Program Analyzers and Verifiers (Dagstuhl Seminar 25242)}},
  pages =	{69--83},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{6},
  editor =	{Christakis, Maria and Donaldson, Alastair F. and Regehr, John and Sotiropoulos, Thodoris},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.6.69},
  URN =		{urn:nbn:de:0030-drops-255761},
  doi =		{10.4230/DagRep.15.6.69},
  annote =	{Keywords: formal methods, program analysis, static analysis, testing, verification}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2019.8

Static Analysis for Asynchronous JavaScript Programs

Authors: Thodoris Sotiropoulos and Benjamin Livshits

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

Abstract

Asynchrony has become an inherent element of JavaScript, as an effort to improve the scalability and performance of modern web applications. To this end, JavaScript provides programmers with a wide range of constructs and features for developing code that performs asynchronous computations, including but not limited to timers, promises, and non-blocking I/O. However, the data flow imposed by asynchrony is implicit, and not always well-understood by the developers who introduce many asynchrony-related bugs to their programs. Worse, there are few tools and techniques available for analyzing and reasoning about such asynchronous applications. In this work, we address this issue by designing and implementing one of the first static analysis schemes capable of dealing with almost all the asynchronous primitives of JavaScript up to the 7th edition of the ECMAScript specification. Specifically, we introduce the callback graph, a representation for capturing data flow between asynchronous code. We exploit the callback graph for designing a more precise analysis that respects the execution order between different asynchronous functions. We parameterize our analysis with one novel context-sensitivity flavor, and we end up with multiple analysis variations for building callback graph. We performed a number of experiments on a set of hand-written and real-world JavaScript programs. Our results show that our analysis can be applied to medium-sized programs achieving 79% precision, on average. The findings further suggest that analysis sensitivity is beneficial for the vast majority of the benchmarks. Specifically, it is able to improve precision by up to 28.5%, while it achieves an 88% precision on average without highly sacrificing performance.

Cite as

Thodoris Sotiropoulos and Benjamin Livshits. Static Analysis for Asynchronous JavaScript Programs. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sotiropoulos_et_al:LIPIcs.ECOOP.2019.8,
  author =	{Sotiropoulos, Thodoris and Livshits, Benjamin},
  title =	{{Static Analysis for Asynchronous JavaScript Programs}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{8:1--8:29},
  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.8},
  URN =		{urn:nbn:de:0030-drops-108007},
  doi =		{10.4230/LIPIcs.ECOOP.2019.8},
  annote =	{Keywords: static analysis, asynchrony, JavaScript}
}

Search Results

Documents authored by Sotiropoulos, Thodoris

Testing Program Analyzers and Verifiers (Dagstuhl Seminar 25242)

Abstract

Cite as

Static Analysis for Asynchronous JavaScript Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message