2 Search Results for "Musuvathi, Madanlal"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.26
Optimal Concolic Dynamic Partial Order Reduction

Authors: Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

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

Abstract
Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.
Cite as

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
  author =	{Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
  title =	{{Optimal Concolic Dynamic Partial Order Reduction}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{26:1--26:22},
  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.26},
  URN =		{urn:nbn:de:0030-drops-239765},
  doi =		{10.4230/LIPIcs.CONCUR.2025.26},
  annote =	{Keywords: Stateless model checking, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.177
The Silently Shifting Semicolon

Authors: Daniel Marino, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, and Abhayendra Singh

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

Abstract
Memory consistency models for modern concurrent languages have largely been designed from a system-centric point of view that protects, at all costs, optimizations that were originally designed for sequential programs. The result is a situation that, when viewed from a programmer's standpoint, borders on absurd. We illustrate this unfortunate situation with a brief fable and then examine the opportunities to right our path.
Cite as

Daniel Marino, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, and Abhayendra Singh. The Silently Shifting Semicolon. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 177-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{marino_et_al:LIPIcs.SNAPL.2015.177,
  author =	{Marino, Daniel and Millstein, Todd and Musuvathi, Madanlal and Narayanasamy, Satish and Singh, Abhayendra},
  title =	{{The Silently Shifting Semicolon}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{177--189},
  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.177},
  URN =		{urn:nbn:de:0030-drops-50259},
  doi =		{10.4230/LIPIcs.SNAPL.2015.177},
  annote =	{Keywords: memory consistency models; sequential consistency; safe programming languages; data races}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2015

  • Refine by Author
  • 1 Khoshechin Jorshari, Mohammad Hossein
  • 1 Kokologiannakis, Michalis
  • 1 Majumdar, Rupak
  • 1 Marino, Daniel
  • 1 Millstein, Todd
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 Stateless model checking
  • 1 dynamic symbolic execution
  • 1 memory consistency models; sequential consistency; safe programming languages; data races

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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact