Search Results

Documents authored by Le, Hoang M.

Found 2 Possible Name Variants:

Le, Hoang M.

Document
DOI: 10.4230/DagSemProc.09461.2
Formal Verification of Abstract SystemC Models

Authors: Daniel Grosse, Hoang M. Le, and Rolf Drechsler

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
In this paper we present a formal verification approach for abstract SystemC models. The approach allows checking expressive properties and lifts induction known from bounded model checking to a higher level, to cope with the large state space of abstract SystemC programs. The technique is tightly integrated with our SystemC to C transformation and generation of monitoring logic to form a complete and efficient method. Properties specifying both hardware and software aspects, e.g. pre- and post-conditions as well as temporal relations of transactions and events, can be specified. As shown by experiments modern proof techniques allow verifying important non-trivial behavior. Moreover, our inductive technique gives significant speed-ups in comparison to simple methods.
Cite as

Daniel Grosse, Hoang M. Le, and Rolf Drechsler. Formal Verification of Abstract SystemC Models. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{grosse_et_al:DagSemProc.09461.2,
  author =	{Grosse, Daniel and Le, Hoang M. and Drechsler, Rolf},
  title =	{{Formal Verification of Abstract SystemC Models}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.2},
  URN =		{urn:nbn:de:0030-drops-25102},
  doi =		{10.4230/DagSemProc.09461.2},
  annote =	{Keywords: SystemC, TLM, BMC, SAT, SMT}
}

Le, Hoang-Oanh

Document
DOI: 10.4230/LIPIcs.MFCS.2022.68
Complexity of the Cluster Vertex Deletion Problem on H-Free Graphs

Authors: Hoang-Oanh Le and Van Bang Le

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The well-known Cluster Vertex Deletion problem (cluster-vd) asks for a given graph G and an integer k whether it is possible to delete at most k vertices of G such that the resulting graph is a cluster graph (a disjoint union of cliques). We give a complete characterization of graphs H for which cluster-vd on H-free graphs is polynomially solvable and for which it is NP-complete.
Cite as

Hoang-Oanh Le and Van Bang Le. Complexity of the Cluster Vertex Deletion Problem on H-Free Graphs. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 68:1-68:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.MFCS.2022.68,
  author =	{Le, Hoang-Oanh and Le, Van Bang},
  title =	{{Complexity of the Cluster Vertex Deletion Problem on H-Free Graphs}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{68:1--68:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.68},
  URN =		{urn:nbn:de:0030-drops-168663},
  doi =		{10.4230/LIPIcs.MFCS.2022.68},
  annote =	{Keywords: Cluster vertex deletion, Vertex cover, Computational complexity, Complexity dichotomy}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.13
Constrained Representations of Map Graphs and Half-Squares

Authors: Hoang-Oanh Le and Van Bang Le

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
The square of a graph H, denoted H^2, is obtained from H by adding new edges between two distinct vertices whenever their distance in H is two. The half-squares of a bipartite graph B=(X,Y,E_B) are the subgraphs of B^2 induced by the color classes X and Y, B^2[X] and B^2[Y]. For a given graph G=(V,E_G), if G=B^2[V] for some bipartite graph B=(V,W,E_B), then B is a representation of G and W is the set of points in B. If in addition B is planar, then G is also called a map graph and B is a witness of G [Chen, Grigni, Papadimitriou. Map graphs. J. ACM , 49 (2) (2002) 127-138]. While Chen, Grigni, Papadimitriou proved that any map graph G=(V,E_G) has a witness with at most 3|V|-6 points, we show that, given a map graph G and an integer k, deciding if G admits a witness with at most k points is NP-complete. As a by-product, we obtain NP-completeness of edge clique partition on planar graphs; until this present paper, the complexity status of edge clique partition for planar graphs was previously unknown. We also consider half-squares of tree-convex bipartite graphs and prove the following complexity dichotomy: Given a graph G=(V,E_G) and an integer k, deciding if G=B^2[V] for some tree-convex bipartite graph B=(V,W,E_B) with |W|<=k points is NP-complete if G is non-chordal dually chordal and solvable in linear time otherwise. Our proof relies on a characterization of half-squares of tree-convex bipartite graphs, saying that these are precisely the chordal and dually chordal graphs.
Cite as

Hoang-Oanh Le and Van Bang Le. Constrained Representations of Map Graphs and Half-Squares. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.MFCS.2019.13,
  author =	{Le, Hoang-Oanh and Le, Van Bang},
  title =	{{Constrained Representations of Map Graphs and Half-Squares}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.13},
  URN =		{urn:nbn:de:0030-drops-109574},
  doi =		{10.4230/LIPIcs.MFCS.2019.13},
  annote =	{Keywords: map graph, half-square, edge clique cover, edge clique partition, graph classes}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2016.50
On the Complexity of Matching Cut in Graphs of Fixed Diameter

Authors: Hoang-Oanh Le and Van Bang Le

Published in: LIPIcs, Volume 64, 27th International Symposium on Algorithms and Computation (ISAAC 2016)

Abstract
In a graph, a matching cut is an edge cut that is a matching. Matching Cut is the problem of deciding whether or not a given graph has a matching cut, which is known to be NP-complete even when restricted to bipartite graphs. It has been proved that Matching Cut is polynomially solvable for graphs of diameter two. In this paper, we show that, for any fixed integer d geq 4, Matching Cut is NP-complete in the class of graphs of diameter d. This almost resolves an open problem posed by Borowiecki and Jesse-Józefczyk in [Matching cutsets in graphs of diameter 2, Theoretical Computer Science 407 (2008) 574-582]. We then show that, for any fixed integer d geq 5, Matching Cut is NP-complete even when restricted to the class of bipartite graphs of diameter d. Complementing the hardness results, we show that Matching Cut is in polynomial-time solvable in the class of bipartite graphs of diameter at most three, and point out a new and simple polynomial-time algorithm solving Matching Cut in graphs of diameter 2.
Cite as

Hoang-Oanh Le and Van Bang Le. On the Complexity of Matching Cut in Graphs of Fixed Diameter. In 27th International Symposium on Algorithms and Computation (ISAAC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 64, pp. 50:1-50:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.ISAAC.2016.50,
  author =	{Le, Hoang-Oanh and Le, Van Bang},
  title =	{{On the Complexity of Matching Cut in Graphs of Fixed Diameter}},
  booktitle =	{27th International Symposium on Algorithms and Computation (ISAAC 2016)},
  pages =	{50:1--50:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-026-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{64},
  editor =	{Hong, Seok-Hee},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2016.50},
  URN =		{urn:nbn:de:0030-drops-68205},
  doi =		{10.4230/LIPIcs.ISAAC.2016.50},
  annote =	{Keywords: matching cut, NP-hardness, graph algorithm, computational complexity, decomposable graph}
}
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