Search Results

Documents authored by Barnat, Jirí

Found 2 Possible Name Variants:

Barnat, Jiri

Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.50
Tunable Online MUS/MSS Enumeration

Authors: Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifiability. Minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform the current state-of-the art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.
Cite as

Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat. Tunable Online MUS/MSS Enumeration. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 50:1-50:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bendik_et_al:LIPIcs.FSTTCS.2016.50,
  author =	{Bend{\'\i}k, Jaroslav and Benes, Nikola and Cern\'{a}, Ivana and Barnat, Jir{\'\i}},
  title =	{{Tunable Online MUS/MSS Enumeration}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{50:1--50:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.50},
  URN =		{urn:nbn:de:0030-drops-68855},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.50},
  annote =	{Keywords: Minimal unsatisfiable subsets, Maximal satisfiable subsets, Unsatisfiab- ility analysis, Infeasibility analysis}
}
Document
DOI: 10.4230/DagSemProc.08332.4
Efficient Large-Scale Model Checking

Authors: Kees Verstoep, Henri E. Bal, Jiri Barnat, and Lubos Brim

Published in: Dagstuhl Seminar Proceedings, Volume 8332, Distributed Verification and Grid Computing (2008)

Abstract
Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment.
Cite as

Kees Verstoep, Henri E. Bal, Jiri Barnat, and Lubos Brim. Efficient Large-Scale Model Checking. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{verstoep_et_al:DagSemProc.08332.4,
  author =	{Verstoep, Kees and Bal, Henri E. and Barnat, Jiri and Brim, Lubos},
  title =	{{Efficient Large-Scale Model Checking}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.4},
  URN =		{urn:nbn:de:0030-drops-16309},
  doi =		{10.4230/DagSemProc.08332.4},
  annote =	{Keywords: Distributed model checking, Grid-based model checking}
}

Barnat, Jirí

Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.50
Tunable Online MUS/MSS Enumeration

Authors: Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifiability. Minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform the current state-of-the art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.
Cite as

Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat. Tunable Online MUS/MSS Enumeration. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 50:1-50:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bendik_et_al:LIPIcs.FSTTCS.2016.50,
  author =	{Bend{\'\i}k, Jaroslav and Benes, Nikola and Cern\'{a}, Ivana and Barnat, Jir{\'\i}},
  title =	{{Tunable Online MUS/MSS Enumeration}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{50:1--50:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.50},
  URN =		{urn:nbn:de:0030-drops-68855},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.50},
  annote =	{Keywords: Minimal unsatisfiable subsets, Maximal satisfiable subsets, Unsatisfiab- ility analysis, Infeasibility analysis}
}
Document
DOI: 10.4230/DagSemProc.08332.4
Efficient Large-Scale Model Checking

Authors: Kees Verstoep, Henri E. Bal, Jiri Barnat, and Lubos Brim

Published in: Dagstuhl Seminar Proceedings, Volume 8332, Distributed Verification and Grid Computing (2008)

Abstract
Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment.
Cite as

Kees Verstoep, Henri E. Bal, Jiri Barnat, and Lubos Brim. Efficient Large-Scale Model Checking. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{verstoep_et_al:DagSemProc.08332.4,
  author =	{Verstoep, Kees and Bal, Henri E. and Barnat, Jiri and Brim, Lubos},
  title =	{{Efficient Large-Scale Model Checking}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.4},
  URN =		{urn:nbn:de:0030-drops-16309},
  doi =		{10.4230/DagSemProc.08332.4},
  annote =	{Keywords: Distributed model checking, Grid-based model checking}
}
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