Found 3 Possible Name Variants:

Document

**Published in:** LIPIcs, Volume 181, 31st International Symposium on Algorithms and Computation (ISAAC 2020)

In this paper, we present primal-dual algorithms for online problems with non-convex objectives. Problems with convex objectives have been extensively studied in recent years where the analyses rely crucially on the convexity and the Fenchel duality. However, problems with non-convex objectives resist against current approaches and non-convexity represents a strong barrier in optimization in general and in the design of online algorithms in particular. In our approach, we consider configuration linear programs with the multilinear extension of the objectives. We follow the multiplicative weight update framework in which a novel point is that the primal update is defined based on the gradient of the multilinear extension. We introduce new notions, namely (local) smoothness, in order to characterize the competitive ratios of our algorithms. The approach leads to competitive algorithms for several problems with convex/non-convex objectives.

Nguyễn Kim Thắng. Online Primal-Dual Algorithms with Configuration Linear Programs. In 31st International Symposium on Algorithms and Computation (ISAAC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 181, pp. 45:1-45:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{thang:LIPIcs.ISAAC.2020.45, author = {Thắng, Nguy\~{ê}n Kim}, title = {{Online Primal-Dual Algorithms with Configuration Linear Programs}}, booktitle = {31st International Symposium on Algorithms and Computation (ISAAC 2020)}, pages = {45:1--45:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-173-3}, ISSN = {1868-8969}, year = {2020}, volume = {181}, editor = {Cao, Yixin and Cheng, Siu-Wing and Li, Minming}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2020.45}, URN = {urn:nbn:de:0030-drops-133891}, doi = {10.4230/LIPIcs.ISAAC.2020.45}, annote = {Keywords: Configuration Linear Programs, Primal-Dual, Smoothness} }

Document

**Published in:** LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

We consider a scheduling problem on unrelated machines with precedence constraints. There are m unrelated machines and n jobs and every job has to be processed non-preemptively in some machine. Moreover, jobs have precedence constraints; specifically, a precedence constraint j ≺ j' requires that job j' can only be started whenever job j has been completed. The objective is to minimize the total completion time.
The problem has been widely studied in more restricted machine environments such as identical or related machines. However, for unrelated machines, much less is known. In the paper, we study the problem where the precedence constraints form a forest of arborescences. We present a O((log n)² / (log log n)³)-approximation algorithm - that improves the best-known guarantee of O((log n)² / log log n) due to Kumar et al. a decade ago. The analysis relies on a dual-fitting method in analyzing the Lagrangian function of non-convex programs.

Nguyễn Kim Thắng. An Improved Approximation Algorithm for Scheduling Under Arborescence Precedence Constraints. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 84:1-84:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{thang:LIPIcs.MFCS.2020.84, author = {Thắng, Nguy\~{ê}n Kim}, title = {{An Improved Approximation Algorithm for Scheduling Under Arborescence Precedence Constraints}}, booktitle = {45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)}, pages = {84:1--84:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-159-7}, ISSN = {1868-8969}, year = {2020}, volume = {170}, editor = {Esparza, Javier and Kr\'{a}l', Daniel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.84}, URN = {urn:nbn:de:0030-drops-127459}, doi = {10.4230/LIPIcs.MFCS.2020.84}, annote = {Keywords: Scheduling, Precedence Constraints, Lagrangian Duality} }

Document

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

We consider the problem of scheduling jobs to minimize the maximum weighted flow-time on a set of related machines. When jobs can be preempted this problem is well-understood; for example, there exists a constant competitive algorithm using speed augmentation. When jobs must be scheduled non-preemptively, only hardness results are known. In this paper, we present the first online guarantees for the non-preemptive variant. We present the first constant competitive algorithm for minimizing the maximum weighted flow-time on related machines by relaxing the problem and assuming that the online algorithm can reject a small fraction of the total weight of jobs. This is essentially the best result possible given the strong lower bounds on the non-preemptive problem without rejection.

Giorgio Lucarelli, Benjamin Moseley, Nguyen Kim Thang, Abhinav Srivastav, and Denis Trystram. Online Non-Preemptive Scheduling to Minimize Maximum Weighted Flow-Time on Related Machines. 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. 24:1-24:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lucarelli_et_al:LIPIcs.FSTTCS.2019.24, author = {Lucarelli, Giorgio and Moseley, Benjamin and Thang, Nguyen Kim and Srivastav, Abhinav and Trystram, Denis}, title = {{Online Non-Preemptive Scheduling to Minimize Maximum Weighted Flow-Time on Related Machines}}, booktitle = {39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)}, pages = {24:1--24:12}, 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.24}, URN = {urn:nbn:de:0030-drops-115867}, doi = {10.4230/LIPIcs.FSTTCS.2019.24}, annote = {Keywords: Online Algorithms, Scheduling, Resource Augmentation} }

Document

**Published in:** LIPIcs, Volume 112, 26th Annual European Symposium on Algorithms (ESA 2018)

In this paper, we consider the online problem of scheduling independent jobs non-preemptively so as to minimize the weighted flow-time on a set of unrelated machines. There has been a considerable amount of work on this problem in the preemptive setting where several competitive algorithms are known in the classical competitive model. However, the problem in the non-preemptive setting admits a strong lower bound. Recently, Lucarelli et al. presented an algorithm that achieves a O(1/epsilon^2)-competitive ratio when the algorithm is allowed to reject epsilon-fraction of total weight of jobs and has an epsilon-speed augmentation. They further showed that speed augmentation alone is insufficient to derive any competitive algorithm. An intriguing open question is whether there exists a scalable competitive algorithm that rejects a small fraction of total weights.
In this paper, we affirmatively answer this question. Specifically, we show that there exists a O(1/epsilon^3)-competitive algorithm for minimizing weighted flow-time on a set of unrelated machine that rejects at most O(epsilon)-fraction of total weight of jobs. The design and analysis of the algorithm is based on the primal-dual technique. Our result asserts that alternative models beyond speed augmentation should be explored when designing online schedulers in the non-preemptive setting in an effort to find provably good algorithms.

Giorgio Lucarelli, Benjamin Moseley, Nguyen Kim Thang, Abhinav Srivastav, and Denis Trystram. Online Non-Preemptive Scheduling to Minimize Weighted Flow-time on Unrelated Machines. In 26th Annual European Symposium on Algorithms (ESA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 112, pp. 59:1-59:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lucarelli_et_al:LIPIcs.ESA.2018.59, author = {Lucarelli, Giorgio and Moseley, Benjamin and Thang, Nguyen Kim and Srivastav, Abhinav and Trystram, Denis}, title = {{Online Non-Preemptive Scheduling to Minimize Weighted Flow-time on Unrelated Machines}}, booktitle = {26th Annual European Symposium on Algorithms (ESA 2018)}, pages = {59:1--59:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-081-1}, ISSN = {1868-8969}, year = {2018}, volume = {112}, editor = {Azar, Yossi and Bast, Hannah and Herman, Grzegorz}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2018.59}, URN = {urn:nbn:de:0030-drops-95226}, doi = {10.4230/LIPIcs.ESA.2018.59}, annote = {Keywords: Online Algorithms, Scheduling, Resource Augmentation} }

Document

**Published in:** LIPIcs, Volume 101, 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)

In the subspace approximation problem, given m points in R^{n} and an integer k <= n, the goal is to find a k-dimension subspace of R^{n} that minimizes the l_{p}-norm of the Euclidean distances to the given points. This problem generalizes several subspace approximation problems and has applications from statistics, machine learning, signal processing to biology. Deshpande et al. [Deshpande et al., 2011] gave a randomized O(sqrt{p})-approximation and this bound is proved to be tight assuming NP != P by Guruswami et al. [Guruswami et al., 2016]. It is an intriguing question of determining the performance guarantee of deterministic algorithms for the problem. In this paper, we present a simple deterministic O(sqrt{p})-approximation algorithm with also a simple analysis. That definitely settles the status of the problem in term of approximation up to a constant factor. Besides, the simplicity of the algorithm makes it practically appealing.

Nguyen Kim Thang. A Greedy Algorithm for Subspace Approximation Problem. In 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 101, pp. 30:1-30:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{thang:LIPIcs.SWAT.2018.30, author = {Thang, Nguyen Kim}, title = {{A Greedy Algorithm for Subspace Approximation Problem}}, booktitle = {16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)}, pages = {30:1--30:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-068-2}, ISSN = {1868-8969}, year = {2018}, volume = {101}, editor = {Eppstein, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2018.30}, URN = {urn:nbn:de:0030-drops-88562}, doi = {10.4230/LIPIcs.SWAT.2018.30}, annote = {Keywords: Approximation Algorithms, Subspace Approximation} }

Document

**Published in:** LIPIcs, Volume 181, 31st International Symposium on Algorithms and Computation (ISAAC 2020)

In this paper, we present primal-dual algorithms for online problems with non-convex objectives. Problems with convex objectives have been extensively studied in recent years where the analyses rely crucially on the convexity and the Fenchel duality. However, problems with non-convex objectives resist against current approaches and non-convexity represents a strong barrier in optimization in general and in the design of online algorithms in particular. In our approach, we consider configuration linear programs with the multilinear extension of the objectives. We follow the multiplicative weight update framework in which a novel point is that the primal update is defined based on the gradient of the multilinear extension. We introduce new notions, namely (local) smoothness, in order to characterize the competitive ratios of our algorithms. The approach leads to competitive algorithms for several problems with convex/non-convex objectives.

Nguyễn Kim Thắng. Online Primal-Dual Algorithms with Configuration Linear Programs. In 31st International Symposium on Algorithms and Computation (ISAAC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 181, pp. 45:1-45:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{thang:LIPIcs.ISAAC.2020.45, author = {Thắng, Nguy\~{ê}n Kim}, title = {{Online Primal-Dual Algorithms with Configuration Linear Programs}}, booktitle = {31st International Symposium on Algorithms and Computation (ISAAC 2020)}, pages = {45:1--45:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-173-3}, ISSN = {1868-8969}, year = {2020}, volume = {181}, editor = {Cao, Yixin and Cheng, Siu-Wing and Li, Minming}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2020.45}, URN = {urn:nbn:de:0030-drops-133891}, doi = {10.4230/LIPIcs.ISAAC.2020.45}, annote = {Keywords: Configuration Linear Programs, Primal-Dual, Smoothness} }

Document

**Published in:** LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

We consider a scheduling problem on unrelated machines with precedence constraints. There are m unrelated machines and n jobs and every job has to be processed non-preemptively in some machine. Moreover, jobs have precedence constraints; specifically, a precedence constraint j ≺ j' requires that job j' can only be started whenever job j has been completed. The objective is to minimize the total completion time.
The problem has been widely studied in more restricted machine environments such as identical or related machines. However, for unrelated machines, much less is known. In the paper, we study the problem where the precedence constraints form a forest of arborescences. We present a O((log n)² / (log log n)³)-approximation algorithm - that improves the best-known guarantee of O((log n)² / log log n) due to Kumar et al. a decade ago. The analysis relies on a dual-fitting method in analyzing the Lagrangian function of non-convex programs.

Nguyễn Kim Thắng. An Improved Approximation Algorithm for Scheduling Under Arborescence Precedence Constraints. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 84:1-84:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{thang:LIPIcs.MFCS.2020.84, author = {Thắng, Nguy\~{ê}n Kim}, title = {{An Improved Approximation Algorithm for Scheduling Under Arborescence Precedence Constraints}}, booktitle = {45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)}, pages = {84:1--84:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-159-7}, ISSN = {1868-8969}, year = {2020}, volume = {170}, editor = {Esparza, Javier and Kr\'{a}l', Daniel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.84}, URN = {urn:nbn:de:0030-drops-127459}, doi = {10.4230/LIPIcs.MFCS.2020.84}, annote = {Keywords: Scheduling, Precedence Constraints, Lagrangian Duality} }

Document

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

We consider the problem of scheduling jobs to minimize the maximum weighted flow-time on a set of related machines. When jobs can be preempted this problem is well-understood; for example, there exists a constant competitive algorithm using speed augmentation. When jobs must be scheduled non-preemptively, only hardness results are known. In this paper, we present the first online guarantees for the non-preemptive variant. We present the first constant competitive algorithm for minimizing the maximum weighted flow-time on related machines by relaxing the problem and assuming that the online algorithm can reject a small fraction of the total weight of jobs. This is essentially the best result possible given the strong lower bounds on the non-preemptive problem without rejection.

Giorgio Lucarelli, Benjamin Moseley, Nguyen Kim Thang, Abhinav Srivastav, and Denis Trystram. Online Non-Preemptive Scheduling to Minimize Maximum Weighted Flow-Time on Related Machines. 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. 24:1-24:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lucarelli_et_al:LIPIcs.FSTTCS.2019.24, author = {Lucarelli, Giorgio and Moseley, Benjamin and Thang, Nguyen Kim and Srivastav, Abhinav and Trystram, Denis}, title = {{Online Non-Preemptive Scheduling to Minimize Maximum Weighted Flow-Time on Related Machines}}, booktitle = {39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)}, pages = {24:1--24:12}, 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.24}, URN = {urn:nbn:de:0030-drops-115867}, doi = {10.4230/LIPIcs.FSTTCS.2019.24}, annote = {Keywords: Online Algorithms, Scheduling, Resource Augmentation} }

Document

**Published in:** LIPIcs, Volume 112, 26th Annual European Symposium on Algorithms (ESA 2018)

In this paper, we consider the online problem of scheduling independent jobs non-preemptively so as to minimize the weighted flow-time on a set of unrelated machines. There has been a considerable amount of work on this problem in the preemptive setting where several competitive algorithms are known in the classical competitive model. However, the problem in the non-preemptive setting admits a strong lower bound. Recently, Lucarelli et al. presented an algorithm that achieves a O(1/epsilon^2)-competitive ratio when the algorithm is allowed to reject epsilon-fraction of total weight of jobs and has an epsilon-speed augmentation. They further showed that speed augmentation alone is insufficient to derive any competitive algorithm. An intriguing open question is whether there exists a scalable competitive algorithm that rejects a small fraction of total weights.
In this paper, we affirmatively answer this question. Specifically, we show that there exists a O(1/epsilon^3)-competitive algorithm for minimizing weighted flow-time on a set of unrelated machine that rejects at most O(epsilon)-fraction of total weight of jobs. The design and analysis of the algorithm is based on the primal-dual technique. Our result asserts that alternative models beyond speed augmentation should be explored when designing online schedulers in the non-preemptive setting in an effort to find provably good algorithms.

Giorgio Lucarelli, Benjamin Moseley, Nguyen Kim Thang, Abhinav Srivastav, and Denis Trystram. Online Non-Preemptive Scheduling to Minimize Weighted Flow-time on Unrelated Machines. In 26th Annual European Symposium on Algorithms (ESA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 112, pp. 59:1-59:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lucarelli_et_al:LIPIcs.ESA.2018.59, author = {Lucarelli, Giorgio and Moseley, Benjamin and Thang, Nguyen Kim and Srivastav, Abhinav and Trystram, Denis}, title = {{Online Non-Preemptive Scheduling to Minimize Weighted Flow-time on Unrelated Machines}}, booktitle = {26th Annual European Symposium on Algorithms (ESA 2018)}, pages = {59:1--59:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-081-1}, ISSN = {1868-8969}, year = {2018}, volume = {112}, editor = {Azar, Yossi and Bast, Hannah and Herman, Grzegorz}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2018.59}, URN = {urn:nbn:de:0030-drops-95226}, doi = {10.4230/LIPIcs.ESA.2018.59}, annote = {Keywords: Online Algorithms, Scheduling, Resource Augmentation} }

Document

**Published in:** LIPIcs, Volume 101, 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)

In the subspace approximation problem, given m points in R^{n} and an integer k <= n, the goal is to find a k-dimension subspace of R^{n} that minimizes the l_{p}-norm of the Euclidean distances to the given points. This problem generalizes several subspace approximation problems and has applications from statistics, machine learning, signal processing to biology. Deshpande et al. [Deshpande et al., 2011] gave a randomized O(sqrt{p})-approximation and this bound is proved to be tight assuming NP != P by Guruswami et al. [Guruswami et al., 2016]. It is an intriguing question of determining the performance guarantee of deterministic algorithms for the problem. In this paper, we present a simple deterministic O(sqrt{p})-approximation algorithm with also a simple analysis. That definitely settles the status of the problem in term of approximation up to a constant factor. Besides, the simplicity of the algorithm makes it practically appealing.

Nguyen Kim Thang. A Greedy Algorithm for Subspace Approximation Problem. In 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 101, pp. 30:1-30:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{thang:LIPIcs.SWAT.2018.30, author = {Thang, Nguyen Kim}, title = {{A Greedy Algorithm for Subspace Approximation Problem}}, booktitle = {16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)}, pages = {30:1--30:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-068-2}, ISSN = {1868-8969}, year = {2018}, volume = {101}, editor = {Eppstein, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2018.30}, URN = {urn:nbn:de:0030-drops-88562}, doi = {10.4230/LIPIcs.SWAT.2018.30}, annote = {Keywords: Approximation Algorithms, Subspace Approximation} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)

There are many powerful techniques for automated termination analysis of
term rewrite systems (TRSs). However, up to now they have hardly been used
for real programming languages. In this talk, we describe recent results
which permit the application of existing techniques from term rewriting
in order to prove termination of programs. We discuss two possible approaches:
1. One could translate programs into TRSs and then use existing tools to
verify termination of the resulting TRSs.
2. One could adapt TRS-techniques to the respective programming languages
in order to analyze programs directly.
We present such approaches for the functional language Haskell and the logic
language Prolog. Our results have been implemented in the termination provers
AProVE and Polytool. In order to handle termination problems resulting
from real programs, these provers had to be coupled with modern SAT solvers,
since the automation of the TRS-termination techniques had to
improve significantly. Our resulting termination analyzers are currently
the most powerful ones for Haskell and Prolog.

Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Daniel De Schreye, and Alexander Serebrenik. Termination of Programs using Term Rewriting and SAT Solving. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{giesl_et_al:DagSemProc.07401.7, author = {Giesl, J\"{u}rgen and Schneider-Kamp, Peter and Thiemann, Ren\'{e} and Swiderski, Stephan and Nguyen, Manh Thang and De Schreye, Daniel and Serebrenik, Alexander}, title = {{Termination of Programs using Term Rewriting and SAT Solving}}, booktitle = {Deduction and Decision Procedures}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.7}, URN = {urn:nbn:de:0030-drops-12481}, doi = {10.4230/DagSemProc.07401.7}, annote = {Keywords: Termination, Term Rewriting, Haskell, Prolog, SAT Solving} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail