5 Search Results for "Gulwani, Sumit"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.7
Combining Generalization Algorithms in Regular Collapse-Free Theories

Authors: Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.
Cite as

Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2025.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Cerna, David M. and Kutsia, Temur and Ringeissen, Christophe},
  title =	{{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.7},
  URN =		{urn:nbn:de:0030-drops-236228},
  doi =		{10.4230/LIPIcs.FSCD.2025.7},
  annote =	{Keywords: Generalization, Anti-unification, Equational theories, Combination}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.10
Bottom-Up Synthesis of Memory Mutations with Separation Logic

Authors: Kasra Ferdowsi and Hila Peleg

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

Abstract
Programming-by-Example (PBE) is the paradigm of program synthesis specified via input-output pairs. It is commonly used because examples are easy to provide and collect from the environment. A popular optimization for enumerative synthesis with examples is Observational Equivalence (OE), which groups programs into equivalence classes according to their evaluation on example inputs. Current formulations of OE, however, are severely limited by the assumption that the synthesizer’s target language contains only pure components with no side-effects, either enforcing this in their target language, or ignoring it, leading to an incorrect enumeration. This limits their ability to use realistic component sets. We address this limitation by borrowing from Separation Logic, which can compositionally reason about heap mutations. We reformulate PBE using a restricted Separation Logic: Concrete Heap Separation Logic (CHSL), transforming the search for programs into a proof search in CHSL. This lets us perform bottom-up enumerative synthesis without the need for expert-provided annotations or domain-specific inferences, but with three key advantages: we (i) preserve correctness in the presence of memory-mutating operations, (ii) compact the search space by representing many concrete programs as one under CHSL, and (iii) perform a provably correct OE-reduction. We present SObEq (Side-effects in OBservational EQuivalence), a bottom-up enumerative algorithm that, given a PBE task, searches for its CHSL derivation. The SObEq algorithm is proved correct with no purity assumptions: we show it is guaranteed to lose no solutions. We also evaluate our implementation of SObEq on benchmarks from the literature and online sources, and show that it produces high-quality results quickly.
Cite as

Kasra Ferdowsi and Hila Peleg. Bottom-Up Synthesis of Memory Mutations with Separation Logic. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferdowsi_et_al:LIPIcs.ECOOP.2025.10,
  author =	{Ferdowsi, Kasra and Peleg, Hila},
  title =	{{Bottom-Up Synthesis of Memory Mutations with Separation Logic}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{10:1--10: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.10},
  URN =		{urn:nbn:de:0030-drops-233036},
  doi =		{10.4230/LIPIcs.ECOOP.2025.10},
  annote =	{Keywords: Program synthesis, observational equivalence}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.11
Semantic Foundations of Equality Saturation

Authors: Dan Suciu, Yisu Remy Wang, and Yihong Zhang

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
Equality saturation is an emerging technique for program and query optimization developed in the programming language community. It performs term rewriting over an E-graph, a data structure that compactly represents a program space. Despite its popularity, the theory of equality saturation lags behind the practice. In this paper, we define a fixpoint semantics of equality saturation based on tree automata and uncover deep connections between equality saturation and the chase. We characterize the class of chase sequences that correspond to equality saturation. We study the complexities of terminations of equality saturation in three cases: single-instance, all-term-instance, and all-E-graph-instance. Finally, we define a syntactic criterion based on acyclicity that implies equality saturation termination.
Cite as

Dan Suciu, Yisu Remy Wang, and Yihong Zhang. Semantic Foundations of Equality Saturation. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{suciu_et_al:LIPIcs.ICDT.2025.11,
  author =	{Suciu, Dan and Wang, Yisu Remy and Zhang, Yihong},
  title =	{{Semantic Foundations of Equality Saturation}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.11},
  URN =		{urn:nbn:de:0030-drops-229523},
  doi =		{10.4230/LIPIcs.ICDT.2025.11},
  annote =	{Keywords: the chase, equality saturation, term rewriting, tree automata, query optimization}
}
Document
DOI: 10.4230/DagRep.3.12.43
Approaches and Applications of Inductive Programming (Dagstuhl Seminar 13502)

Authors: Sumit Gulwani, Emanuel Kitzelmann, and Ute Schmid

Published in: Dagstuhl Reports, Volume 3, Issue 12 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13502 "Approaches and Applications of Inductive Programming". After a short introduction to inductive programming research, an overview of the talks and the outcomes of discussion groups is given.
Cite as

Sumit Gulwani, Emanuel Kitzelmann, and Ute Schmid. Approaches and Applications of Inductive Programming (Dagstuhl Seminar 13502). In Dagstuhl Reports, Volume 3, Issue 12, pp. 43-66, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{gulwani_et_al:DagRep.3.12.43,
  author =	{Gulwani, Sumit and Kitzelmann, Emanuel and Schmid, Ute},
  title =	{{Approaches and Applications of Inductive Programming (Dagstuhl Seminar 13502)}},
  pages =	{43--66},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{12},
  editor =	{Gulwani, Sumit and Kitzelmann, Emanuel and Schmid, Ute},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.12.43},
  URN =		{urn:nbn:de:0030-drops-45078},
  doi =		{10.4230/DagRep.3.12.43},
  annote =	{Keywords: inductive program synthesis, end-user programming, universal artificial intelligence, constraint programming, probabilistic programming, cognitive mod}
}
Document
DOI: 10.4230/DagRep.2.4.21
Software Synthesis (Dagstuhl Seminar 12152)

Authors: Rastislav Bodík, Sumit Gulwani, and Eran Yahav

Published in: Dagstuhl Reports, Volume 2, Issue 4 (2012)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12152 ``Software Synthesis''. During the seminar, several participants presented their current research, ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper. The rise of multiprocesser computers and of software verification as applied in industry combine to create an opportune moment for software synthesis. To facilitate research in this area, research from several fields of Computer Science presented tutorials on techniques they developed. This lead to (1) the definition of what challenges synthesis has to tackle in the future and (2) insights into how the several fields of synthesis are related. Finally, several groups described their experience with teaching synthesis to graduate and undergraduate students, demonstrating that synthesis is challenging for students but that they can also rise to the challenge and enjoy the field.
Cite as

Rastislav Bodík, Sumit Gulwani, and Eran Yahav. Software Synthesis (Dagstuhl Seminar 12152). In Dagstuhl Reports, Volume 2, Issue 4, pp. 21-38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Article{bodik_et_al:DagRep.2.4.21,
  author =	{Bod{\'\i}k, Rastislav and Gulwani, Sumit and Yahav, Eran},
  title =	{{Software Synthesis (Dagstuhl Seminar 12152)}},
  pages =	{21--38},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{2},
  number =	{4},
  editor =	{Bod{\'\i}k, Rastislav and Gulwani, Sumit and Yahav, Eran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.4.21},
  URN =		{urn:nbn:de:0030-drops-35956},
  doi =		{10.4230/DagRep.2.4.21},
  annote =	{Keywords: Software Synthesis, Verification and Model Checking, Theorem Proving, Program Analysis, Programming by Demonstration, Program Derivation, Compiler Optimization}
}
  • Refine by Type
  • 5 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2014
  • 1 2012

  • Refine by Author
  • 2 Gulwani, Sumit
  • 1 Ayala-Rincón, Mauricio
  • 1 Bodík, Rastislav
  • 1 Cerna, David M.
  • 1 Ferdowsi, Kasra
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 2 DagRep

  • Refine by Classification
  • 2 Theory of computation → Equational logic and rewriting
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Software and its engineering → Automatic programming
  • 1 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 1 Anti-unification
  • 1 Combination
  • 1 Compiler Optimization
  • 1 Equational theories
  • 1 Generalization
  • 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