4 Search Results for "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.MFCS.2018.18
Lagrange's Theorem for Binary Squares

Authors: P. Madhusudan, Dirk Nowotka, Aayush Rajasekaran, and Jeffrey Shallit

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. Here the number 4 is optimal. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.
Cite as

P. Madhusudan, Dirk Nowotka, Aayush Rajasekaran, and Jeffrey Shallit. Lagrange's Theorem for Binary Squares. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 18:1-18:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{madhusudan_et_al:LIPIcs.MFCS.2018.18,
  author =	{Madhusudan, P. and Nowotka, Dirk and Rajasekaran, Aayush and Shallit, Jeffrey},
  title =	{{Lagrange's Theorem for Binary Squares}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.18},
  URN =		{urn:nbn:de:0030-drops-96003},
  doi =		{10.4230/LIPIcs.MFCS.2018.18},
  annote =	{Keywords: binary square, theorem-proving, finite automaton, decision procedure, decidable theory, additive number theory}
}
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}
}
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}
}
  • Refine by Author
  • 2 Parthasarathy, Madhusudan
  • 1 La Torre, Salvatore
  • 1 Madhusudan, P.
  • 1 Madhusudan, Parthasarathy
  • 1 Nowotka, Dirk
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Discrete mathematics
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 1 Verification
  • 1 additive number theory
  • 1 automata theory
  • 1 binary square
  • 1 boolean programs
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2011
  • 1 2012
  • 1 2018
  • 1 2019

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact