4 Search Results for "Raychev, Veselin"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.22
Partial-Order Reduction Is Hard

Authors: Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective. In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time.
Cite as

Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz. Partial-Order Reduction Is Hard. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2025.22,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Larroze-Jardin\'{e}, Sarah and Walukiewicz, Igor},
  title =	{{Partial-Order Reduction Is Hard}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22},
  URN =		{urn:nbn:de:0030-drops-239727},
  doi =		{10.4230/LIPIcs.CONCUR.2025.22},
  annote =	{Keywords: Formal verification, Concurrent systems, Partial-order reduction, Complexity}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.9
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
DOI: 10.4230/LIPIcs.ECOOP.2025.18
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
DOI: 10.4230/LIPIcs.SNAPL.2015.41
Programming with "Big Code": Lessons, Techniques and Applications

Authors: Pavol Bielik, Veselin Raychev, and Martin Vechev

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Programming tools based on probabilistic models of massive codebases (aka "Big Code") promise to solve important programming tasks that were difficult or practically infeasible to address before. However, building such tools requires solving a number of hard problems at the intersection of programming languages, program analysis and machine learning. In this paper we summarize some of our experiences and insights obtained by developing several such probabilistic systems over the last few years (some of these systems are regularly used by thousands of developers worldwide). We hope these observations can provide a guideline for others attempting to create such systems. We also present a prediction approach we find suitable as a starting point for building probabilistic tools, and discuss a practical framework implementing this approach, called Nice2Predict. We release the Nice2Predict framework publicly - the framework can be immediately used as a basis for developing new probabilistic tools. Finally, we present programming applications that we believe will benefit from probabilistic models and should be investigated further.
Cite as

Pavol Bielik, Veselin Raychev, and Martin Vechev. Programming with "Big Code": Lessons, Techniques and Applications. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 41-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bielik_et_al:LIPIcs.SNAPL.2015.41,
  author =	{Bielik, Pavol and Raychev, Veselin and Vechev, Martin},
  title =	{{Programming with "Big Code": Lessons, Techniques and Applications}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{41--50},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.41},
  URN =		{urn:nbn:de:0030-drops-50152},
  doi =		{10.4230/LIPIcs.SNAPL.2015.41},
  annote =	{Keywords: probabilistic tools, probabilistic inference and learning, program analysis, open-source software}
}
  • Refine by Type
  • 4 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2015

  • Refine by Author
  • 1 Bielik, Pavol
  • 1 Das, Kanak
  • 1 Endo, Andre Takeshi
  • 1 Hassanshahi, Behnaz
  • 1 Herbreteau, Frédéric
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 1 Security and privacy → Software security engineering
  • 1 Software and its engineering → Software testing and debugging
  • 1 Software and its engineering → Software verification and validation
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Complexity
  • 1 Concurrent systems
  • 1 Formal verification
  • 1 Inference
  • 1 JavaScript
  • 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
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact