Search Results

Documents authored by Parthasarathy, Madhusudan

Found 2 Possible Name Variants:

Madhusudan, Parthasarathy

Document
DOI: 10.4230/LIPIcs.CSL.2011.428
Synthesizing Reactive Programs

Authors: Parthasarathy Madhusudan

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Current theoretical solutions to the classical Church's synthesis problem are focused on synthesizing transition systems and not programs. Programs are compact and often the true aim in many synthesis problems, while the transition systems that correspond to them are often large and not very useful as synthesized artefacts. Consequently, current practical techniques first synthesize a transition system, and then extract a more compact representation from it. We reformulate the synthesis of reactive systems directly in terms of program synthesis, and develop a theory to show that the problem of synthesizing programs over a fixed set of Boolean variables in a simple imperative programming language is decidable for regular omega-specifications. We also present results for synthesizing programs with recursion against both regular specifications as well as visibly-pushdown language specifications. Finally, we show applications to program repair, and conclude with open problems in synthesizing distributed programs.
Cite as

Parthasarathy Madhusudan. Synthesizing Reactive Programs. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 428-442, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{madhusudan:LIPIcs.CSL.2011.428,
  author =	{Madhusudan, Parthasarathy},
  title =	{{Synthesizing Reactive Programs}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{428--442},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.428},
  URN =		{urn:nbn:de:0030-drops-32479},
  doi =		{10.4230/LIPIcs.CSL.2011.428},
  annote =	{Keywords: program synthesis, boolean programs, automata theory, temporal logics}
}

Parthasarathy, Madhusudan

Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.46
Reachability in Concurrent Uninterpreted Programs

Authors: Salvatore La Torre and Madhusudan Parthasarathy

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We study the safety verification (reachability problem) for concurrent programs with uninterpreted functions/relations. By extending the notion of coherence, recently identified for sequential programs, to concurrent programs, we show that reachability in coherent concurrent programs under various scheduling restrictions is decidable by a reduction to multistack pushdown automata, and establish precise complexity bounds for them. We also prove that the coherence restriction for these various scheduling restrictions is itself a decidable property.
Cite as

Salvatore La Torre and Madhusudan Parthasarathy. Reachability in Concurrent Uninterpreted Programs. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{latorre_et_al:LIPIcs.FSTTCS.2019.46,
  author =	{La Torre, Salvatore and Parthasarathy, Madhusudan},
  title =	{{Reachability in Concurrent Uninterpreted Programs}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{46:1--46:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.46},
  URN =		{urn:nbn:de:0030-drops-116082},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.46},
  annote =	{Keywords: Verification, uninterpreted programs, concurrent programs, shared memory}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.34
Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures

Authors: Madhusudan Parthasarathy

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
We consider the problem of automatically verifying programs that manipulate a dynamic heap, maintaining complex and multiple data-structures, given modular pre-post conditions and loop invariants. We discuss specification logics for heaps, and discuss two classes of automatic procedures for reasoning with these logics. The first identifies fragments of logics that admit completely decidable reasoning. The second is a new approach called the natural proof method that builds proof procedures for very expressive logics that are automatic and sound (but incomplete), and that embody natural proof tactics learnt from manual verification.
Cite as

Madhusudan Parthasarathy. Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 34-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{parthasarathy:LIPIcs.FSTTCS.2012.34,
  author =	{Parthasarathy, Madhusudan},
  title =	{{Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{34--35},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.34},
  URN =		{urn:nbn:de:0030-drops-38897},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.34},
  annote =	{Keywords: logic, heap structures, data structures, program verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact