Search Results

Documents authored by Prasad, Siddhartha

Document
DOI: 10.4230/LIPIcs.ECOOP.2026.22
Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages

Authors: Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Developers routinely use GenAI tools (large language models enriched in various ways) to generate useful components of programs, such as regular expressions. While pleasant and often effective, this can easily lead to subtle bugs. The developer may have been unclear in their specification, they may not fully understand the language of the output, there may be systematic misconceptions suffered by the user and perhaps even embedded in the language model, and so on. Responsible use of GenAI requires humans in the loop. To be effective, the human interaction must be both meaningful and moderate. We accomplish this as follows. First, we generate multiple candidate expressions instead of one. We then use formal language containment properties to generate distinguishing concrete scenarios that illustrate the differences between the candidates. We then have users rate these concrete scenarios. This process converges in a few steps, while also giving the user insight into any lack of clarity on their part. We have built a tool, pick, that implements this iterative process. We apply it to three formal languages with the necessary properties: regexes, linear temporal logic, and access-control policies. We show through experiments that pick is a significant improvement over showing users the candidate expressions, and also helps catch situations where no output is a match.
Cite as

Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi. Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 22:1-22:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{prasad_et_al:LIPIcs.ECOOP.2026.22,
  author =	{Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
  title =	{{Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{22:1--22:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert 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.2026.22},
  URN =		{urn:nbn:de:0030-drops-261181},
  doi =		{10.4230/LIPIcs.ECOOP.2026.22},
  annote =	{Keywords: Regex, LTL, Access Control, Generative AI, Human-in-the-Loop}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.7
Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact)

Authors: Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This artifact accompanies the paper Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages. It provides (1) the pick VS Code extension for regex synthesis with human-in-the-loop validation, and (2) anonymized user-study data and Docker images that reproduce the study interfaces and statistical analyses reported in the paper.
Cite as

Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi. Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 7:1-7:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{prasad_et_al:DARTS.12.1.7,
  author =	{Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
  title =	{{Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact)}},
  pages =	{7:1--7:9},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.7},
  URN =		{urn:nbn:de:0030-drops-261445},
  doi =		{10.4230/DARTS.12.1.7},
  annote =	{Keywords: Regex, LTL, Access Control, Generative AI, Human-in-the-Loop}
}
Artifact
Software
DOI: 10.4230/artifacts.23608
sidprasad/copeanddrag

Authors: Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi

Abstract
Cite as

Siddhartha Prasad, Ben Greenman, Tim Nelson, Shriram Krishnamurthi. sidprasad/copeanddrag (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23608,
   title = {{sidprasad/copeanddrag}}, 
   author = {Prasad, Siddhartha and Greenman, Ben and Nelson, Tim and Krishnamurthi, Shriram},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b92dbb01ca5fcbe40ac64c8026fb3076fbf85d2a;origin=https://github.com/sidprasad/copeanddrag;visit=swh:1:snp:990270b6e3e85f7a6917e242812969d881a8b6cc;anchor=swh:1:rev:51bd5b858fffd4e8c78791d272293d140c1b2fdb}{\texttt{swh:1:dir:b92dbb01ca5fcbe40ac64c8026fb3076fbf85d2a}} (visited on 2025-06-25)},
   url = {https://github.com/sidprasad/copeanddrag/tree/ecoop-25},
   doi = {10.4230/artifacts.23608},
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.26
Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design

Authors: Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi

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

Abstract
Tools such as Alloy enable users to incrementally define, explore, verify, and diagnose specifications for complex systems. A critical component of these tools is a visualizer that lets users graphically explore generated models. As we show, however, a default visualizer that knows nothing about the domain can be unhelpful and can even actively violate presentational and cognitive principles. At the other extreme, full-blown custom visualization requires significant effort as well as knowledge that a tool user might not possess. Custom visualizations can also exhibit bad (even silent) failures. This paper charts a middle ground between the extremes of default and fully-customizable visualization. We capture essential domain information for lightweight diagramming, embodying this in a language. To identify key elements of lightweight diagrams, we ground the language design in both the cognitive science research on diagrams and in a corpus of 58 custom visualizations. We distill from these sources a small set of orthogonal primitives, and use the primitives to guide a diagramming language called Cope-and-Drag (CnD). We evaluate it on sample tasks, three user studies, and performance, and find that short CnD specifications consistently improve model comprehension over the Alloy default. CnD thus defines a new point in the design space of diagramming: a language that is lightweight, effective, and driven by sound principles.
Cite as

Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi. Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 26:1-26:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{prasad_et_al:LIPIcs.ECOOP.2025.26,
  author =	{Prasad, Siddhartha and Greenman, Ben and Nelson, Tim and Krishnamurthi, Shriram},
  title =	{{Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{26:1--26: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.26},
  URN =		{urn:nbn:de:0030-drops-233187},
  doi =		{10.4230/LIPIcs.ECOOP.2025.26},
  annote =	{Keywords: formal methods, diagramming, visualization, language design}
}
Document
Artifact
DOI: 10.4230/DARTS.11.2.12
Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design (Artifact)

Authors: Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
This artifact supports the paper “Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design.” It provides an implementation of Cope and Drag (CnD), a lightweight diagramming language grounded in cognitive principles and a corpus analysis of existing visualizations. CnD enables users to define diagrams using a small set of orthogonal primitives that capture essential domain structure while avoiding the complexity of writing full visualization programs. The artifact allows exploration of CnD’s implementation and reproduction of claims made in the accompanying paper.
Cite as

Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi. Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 12:1-12:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{prasad_et_al:DARTS.11.2.12,
  author =	{Prasad, Siddhartha and Greenman, Ben and Nelson, Tim and Krishnamurthi, Shriram},
  title =	{{Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design (Artifact)}},
  pages =	{12:1--12:11},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Prasad, Siddhartha and Greenman, Ben and Nelson, Tim and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.12},
  URN =		{urn:nbn:de:0030-drops-233552},
  doi =		{10.4230/DARTS.11.2.12},
  annote =	{Keywords: formal methods, diagramming, visualization, language design}
}
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