6 Search Results for "Dang, Nguyen"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.25
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 25:1-25:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.25,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{25:1--25:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.25},
  URN =		{urn:nbn:de:0030-drops-208741},
  doi =		{10.4230/LIPIcs.ECOOP.2024.25},
  annote =	{Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.16
A Formal Proof of R(4,5)=25

Authors: Thibault Gauthier and Chad E. Brown

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker.
Cite as

Thibault Gauthier and Chad E. Brown. A Formal Proof of R(4,5)=25. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gauthier_et_al:LIPIcs.ITP.2024.16,
  author =	{Gauthier, Thibault and Brown, Chad E.},
  title =	{{A Formal Proof of R(4,5)=25}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.16},
  URN =		{urn:nbn:de:0030-drops-207446},
  doi =		{10.4230/LIPIcs.ITP.2024.16},
  annote =	{Keywords: Ramsey numbers, SAT solvers, symmetry breaking, generalization, HOL4}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CP.2024.1
Solving Patience and Solitaire Games with Good Old Fashioned AI (Invited Talk)

Authors: Ian P. Gent

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
While games like Chess, Checkers and Go have been the subject of extensive research in AI for decades, there has been comparatively little study of single player card games. These games are generally called "Patience" in British English and "Solitaire" in US English, and have been popular for hundreds of years and remain so today. In fact, our ignorance of the winnability percentage of just one such game - "Klondike" - has been described as "one of the embarrassments of applied mathematics" by the distinguished statistician Persi Diaconis. I will talk about "Solvitaire", a program to solve patience games given a simple JSON description of the rules of the game and the initial layout. We have used Solvitaire to determine the winnability percentage of dozens different single-player card games with a 95% confidence interval of ± 0.1% or better. For example, we now know the winnability of Klondike as 81.945% ± 0.084% (in the "thoughtful" variant where the player knows the rank and suit of all cards), a 30-fold reduction in confidence interval over the best previous result. The vast majority of results we obtained with Solvitaire are either entirely new or represent significant improvements on previous knowledge. Solvitaire is very much a "Good Old Fashioned AI" approach to solving patience games, without using Machine Learning or Neural networks. It uses exhaustive depth-first search to explore all possible ways that a game could possibly be won, ensuring that games reported unwinnable really are so. This can involve searching extraordinary seach spaces with depths in the millions even including cases where unwinnability is proven. Numerous techniques imported from AI search play an important role in making this search practicable. Particularly important ones are: the use of a transposition tables; the exploitation of symmetry in search; the use of dominances to force certain moves to be made when it is safe to do so; and the use of streamliners. Solvitaire does have some games it performs poorly on, where exhaustive search is unable to prove that no win is possible but an alternative simple proof is in fact available. I will also talk about using constraint models do this, leading to slight improvements in some variants of Klondike but dramatic improvements in others. This talk will include personal anecdotes, explaining for example why it is dedicated to my mother Margaret Gent (1923-2021) for her patience in teaching me to love the game of patience.
Cite as

Ian P. Gent. Solving Patience and Solitaire Games with Good Old Fashioned AI (Invited Talk). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gent:LIPIcs.CP.2024.1,
  author =	{Gent, Ian P.},
  title =	{{Solving Patience and Solitaire Games with Good Old Fashioned AI}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.1},
  URN =		{urn:nbn:de:0030-drops-206863},
  doi =		{10.4230/LIPIcs.CP.2024.1},
  annote =	{Keywords: AI Search, Solitaire and Patience Games}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2024.38
Frugal Algorithm Selection (Short Paper)

Authors: Erdem Kuş, Özgür Akgün, Nguyen Dang, and Ian Miguel

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
When solving decision and optimisation problems, many competing algorithms (model and solver choices) have complementary strengths. Typically, there is no single algorithm that works well for all instances of a problem. Automated algorithm selection has been shown to work very well for choosing a suitable algorithm for a given instance. However, the cost of training can be prohibitively large due to running candidate algorithms on a representative set of training instances. In this work, we explore reducing this cost by choosing a subset of the training instances on which to train. We approach this problem in three ways: using active learning to decide based on prediction uncertainty, augmenting the algorithm predictors with a timeout predictor, and collecting training data using a progressively increasing timeout. We evaluate combinations of these approaches on six datasets from ASLib and present the reduction in labelling cost achieved by each option.
Cite as

Erdem Kuş, Özgür Akgün, Nguyen Dang, and Ian Miguel. Frugal Algorithm Selection (Short Paper). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kus_et_al:LIPIcs.CP.2024.38,
  author =	{Ku\c{s}, Erdem and Akg\"{u}n, \"{O}zg\"{u}r and Dang, Nguyen and Miguel, Ian},
  title =	{{Frugal Algorithm Selection}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.38},
  URN =		{urn:nbn:de:0030-drops-207239},
  doi =		{10.4230/LIPIcs.CP.2024.38},
  annote =	{Keywords: Algorithm Selection, Active Learning}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.18
A Framework for Generating Informative Benchmark Instances

Authors: Nguyen Dang, Özgür Akgün, Joan Espasa, Ian Miguel, and Peter Nightingale

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
Benchmarking is an important tool for assessing the relative performance of alternative solving approaches. However, the utility of benchmarking is limited by the quantity and quality of the available problem instances. Modern constraint programming languages typically allow the specification of a class-level model that is parameterised over instance data. This separation presents an opportunity for automated approaches to generate instance data that define instances that are graded (solvable at a certain difficulty level for a solver) or can discriminate between two solving approaches. In this paper, we introduce a framework that combines these two properties to generate a large number of benchmark instances, purposely generated for effective and informative benchmarking. We use five problems that were used in the MiniZinc competition to demonstrate the usage of our framework. In addition to producing a ranking among solvers, our framework gives a broader understanding of the behaviour of each solver for the whole instance space; for example by finding subsets of instances where the solver performance significantly varies from its average performance.
Cite as

Nguyen Dang, Özgür Akgün, Joan Espasa, Ian Miguel, and Peter Nightingale. A Framework for Generating Informative Benchmark Instances. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dang_et_al:LIPIcs.CP.2022.18,
  author =	{Dang, Nguyen and Akg\"{u}n, \"{O}zg\"{u}r and Espasa, Joan and Miguel, Ian and Nightingale, Peter},
  title =	{{A Framework for Generating Informative Benchmark Instances}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.18},
  URN =		{urn:nbn:de:0030-drops-166479},
  doi =		{10.4230/LIPIcs.CP.2022.18},
  annote =	{Keywords: Instance generation, Benchmarking, Constraint Programming}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.38
Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

Authors: Felix Ulrich-Oltean, Peter Nightingale, and James Alfred Walker

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.
Cite as

Felix Ulrich-Oltean, Peter Nightingale, and James Alfred Walker. Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ulricholtean_et_al:LIPIcs.CP.2022.38,
  author =	{Ulrich-Oltean, Felix and Nightingale, Peter and Walker, James Alfred},
  title =	{{Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{38:1--38:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.38},
  URN =		{urn:nbn:de:0030-drops-166670},
  doi =		{10.4230/LIPIcs.CP.2022.38},
  annote =	{Keywords: Constraint programming, SAT encodings, machine learning, global constraints, pseudo-Boolean constraints, linear constraints}
}
  • Refine by Author
  • 2 Akgün, Özgür
  • 2 Dang, Nguyen
  • 2 Miguel, Ian
  • 2 Nightingale, Peter
  • 1 Ayoun, Sacha-Élie
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Constraint and logic programming
  • 2 Theory of computation → Automated reasoning
  • 1 Computing methodologies → Discrete space search
  • 1 Theory of computation → Active learning
  • 1 Theory of computation → Program analysis
  • Show More...

  • Refine by Keyword
  • 1 AI Search
  • 1 Active Learning
  • 1 Algorithm Selection
  • 1 Benchmarking
  • 1 Constraint Programming
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 4 2024
  • 2 2022

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