Search Results

Documents authored by Kapur, Deepak

Document
DOI: 10.4230/LIPIcs.FSCD.2021.15
A Modular Associative Commutative (AC) Congruence Closure Algorithm

Authors: Deepak Kapur

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing the congruence closure by abstracting nonflat terms by constants as proposed first in Kapur’s congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combinations. The algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into Satisfiability modulo Theories (SMT) solvers.
Cite as

Deepak Kapur. A Modular Associative Commutative (AC) Congruence Closure Algorithm. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kapur:LIPIcs.FSCD.2021.15,
  author =	{Kapur, Deepak},
  title =	{{A Modular Associative Commutative (AC) Congruence Closure Algorithm}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{15:1--15:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.15},
  URN =		{urn:nbn:de:0030-drops-142530},
  doi =		{10.4230/LIPIcs.FSCD.2021.15},
  annote =	{Keywords: Congruence Closure, Associative and Commutative, Word Problems, Finitely Presented Algebras, Equational Theories}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.41
Termination Analysis of C Programs Using Compiler Intermediate Languages

Authors: Stephan Falke, Deepak Kapur, and Carsten Sinz

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
Modeling the semantics of programming languages like C for the automated termination analysis of programs is a challenge if complete coverage of all language features should be achieved. On the other hand, low-level intermediate languages that occur during the compilation of C programs to machine code have a much simpler semantics since most of the intricacies of C are taken care of by the compiler frontend. It is thus a promising approach to use these intermediate languages for the automated termination analysis of C programs. In this paper we present the tool KITTeL based on this approach. For this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself is then performed on the automatically generated TRS. An evaluation on a large collection of C programs shows the effectiveness and practicality of KITTeL on "typical" examples.
Cite as

Stephan Falke, Deepak Kapur, and Carsten Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 41-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{falke_et_al:LIPIcs.RTA.2011.41,
  author =	{Falke, Stephan and Kapur, Deepak and Sinz, Carsten},
  title =	{{Termination Analysis of C Programs Using Compiler Intermediate Languages}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{41--50},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.41},
  URN =		{urn:nbn:de:0030-drops-31232},
  doi =		{10.4230/LIPIcs.RTA.2011.41},
  annote =	{Keywords: termination analysis; C programs; compiler intermediate languages}
}
Document
DOI: 10.4230/DagSemProc.05431.3
Automatically Generating Loop Invariants Using Quantifier Elimination

Authors: Deepak Kapur

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
An approach for automatically generating loop invariants using quantifier-elimination is proposed. An invariant of a loop is hypothesized as a parameterized formula. Parameters in the invariant are discovered by generating constraints on the parameters by ensuring that the formula is indeed preserved by the execution path corresponding to every basic cycle of the loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition of the loop, if available, can also be used to further refine the hypothesized invariant. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form does not exist for the loop. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the first-order theory of polynomial equations as well as Presburger arithmetic.
Cite as

Deepak Kapur. Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kapur:DagSemProc.05431.3,
  author =	{Kapur, Deepak},
  title =	{{Automatically Generating Loop Invariants Using Quantifier Elimination}},
  booktitle =	{Deduction and Applications},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.3},
  URN =		{urn:nbn:de:0030-drops-5116},
  doi =		{10.4230/DagSemProc.05431.3},
  annote =	{Keywords: Program verification, loop invariants, inductive assertions, quantifier elimination}
}
Document
DOI: 10.4230/DagSemRep.376
Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171)

Authors: Deepak Kapur, Andreas Podelski, and Andrei Voronkov

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Deepak Kapur, Andreas Podelski, and Andrei Voronkov. Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171). Dagstuhl Seminar Report 376, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{kapur_et_al:DagSemRep.376,
  author =	{Kapur, Deepak and Podelski, Andreas and Voronkov, Andrei},
  title =	{{Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171)}},
  pages =	{1--5},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{376},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.376},
  URN =		{urn:nbn:de:0030-drops-152564},
  doi =		{10.4230/DagSemRep.376},
}
Document
DOI: 10.4230/DagSemRep.300
Deduction (Dagstuhl Seminar 01101)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 01101). Dagstuhl Seminar Report 300, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.300,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 01101)}},
  pages =	{1--27},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{300},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.300},
  URN =		{urn:nbn:de:0030-drops-151843},
  doi =		{10.4230/DagSemRep.300},
}
Document
DOI: 10.4230/DagSemRep.232
Deduction (Dagstuhl Seminar 99091)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 99091). Dagstuhl Seminar Report 232, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.232,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 99091)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{232},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.232},
  URN =		{urn:nbn:de:0030-drops-151182},
  doi =		{10.4230/DagSemRep.232},
}
Document
DOI: 10.4230/DagSemRep.122
Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530)

Authors: Alan Bundy, Robert S. Boyer, Deepak Kapur, and Christoph Walther

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Alan Bundy, Robert S. Boyer, Deepak Kapur, and Christoph Walther. Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530). Dagstuhl Seminar Report 122, pp. 1-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1996)

Copy BibTex To Clipboard

@TechReport{bundy_et_al:DagSemRep.122,
  author =	{Bundy, Alan and Boyer, Robert S. and Kapur, Deepak and Walther, Christoph},
  title =	{{Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530)}},
  pages =	{1--40},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{122},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.122},
  URN =		{urn:nbn:de:0030-drops-150107},
  doi =		{10.4230/DagSemRep.122},
}
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 About DROPS Imprint Privacy Contact