MUST: Minimal Unsatisfiable Subsets Enumeration Tool
151
References
1. Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more
efficiently compute minimal unsatisfiable sets. In CAV (2), volume 9207 of LNCS,
pages 70–86. Springer, 2015.
2. Fahiem Bacchus and George Katsirelos. Finding a collection of MUSes incrementally. In CPAIOR, volume 9676 of LNCS, pages 35–44. Springer, 2016.
3. James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of
constraints using hitting set dualization. In PADL, pages 174–186. Springer, 2005.
4. Jiˇ r´ ı Barnat, Petr Bauch, Nikola Beneˇ s, Luboˇ s Brim, Jan Beran, and Tom´ aˇ s Kratochv´ ıla. Analysing sanity of requirements for avionics systems. FAoC, 2016.
5. Anton Belov and Jo˜ ao Marques-Silva. MUSer2: An efficient MUS extractor. JSAT,
8:123–128, 2012.
6. Jaroslav Bend´ ık. Consistency checking in requirements analysis. In ISSTA, pages
408–411. ACM, 2017.
7. Jaroslav Bend´ ık, Nikola Beneˇ s, Ivana ˇ
Cern´ a, and Jiˇ r´ ı Barnat. Tunable online
MUS/MSS enumeration. In FSTTCS, volume 65 of LIPIcs, pages 50:1–50:13.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
8. Jaroslav Bend´ ık and Ivana ˇ
Cern´ a. Evaluation of domain agnostic approaches for
enumeration of minimal unsatisfiable subsets. In LPAR, volume 57 of EPiC Series
in Computing, pages 131–142. EasyChair, 2018.
9. Jaroslav Bend´ ık, Ivana ˇ
Cern´ a, and Nikola Beneˇ s. Recursive online enumeration of
all minimal unsatisfiable subsets. In ATVA, volume 11138 of LNCS, pages 143–159.
Springer, 2018.
10. Jaroslav Bend´ ık, Elaheh Ghassabani, Michael W. Whalen, and Ivana ˇ
Cern´ a. Online
enumeration of all minimal inductive validity cores. In SEFM, volume 10886 of
LNCS, pages 189–204. Springer, 2018.
11. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta.
The nuxmv symbolic model checker. In CAV, volume 8559 of LNCS, pages 334–342.
Springer, 2014.
12. Huan Chen and Jo˜ ao Marques-Silva. Improvements to satisfiability-based boolean
function bi-decomposition. In VLSI-SoC, pages 142–147. IEEE, 2011.
13. Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Computing small
unsatisfiable cores in satisfiability modulo theories. JAIR, 40:701–728, 2011.
14. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
Counterexample-guided abstraction refinement. In CAV, volume 1855 of LNCS,
pages 154–169. Springer, 2000.
15. Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel, and Vadim
Ryvchin. Designers work less with quality formal equivalence checking. In Design and Verification Conference (DVCon). Citeseer, 2010.
16. Leonardo Mendon¸ ca de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver.
In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008.
17. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud
Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - A framework for LTL
and ω-automata manipulation. In ATVA, volume 9938 of LNCS, pages 122–129,
2016.
18. Niklas E´ en and Niklas S¨ orensson. An extensible SAT-solver. In SAT, volume 2919
of LNCS, pages 502–518. Springer, 2003.
151
References
1. Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more
efficiently compute minimal unsatisfiable sets. In CAV (2), volume 9207 of LNCS,
pages 70–86. Springer, 2015.
2. Fahiem Bacchus and George Katsirelos. Finding a collection of MUSes incrementally. In CPAIOR, volume 9676 of LNCS, pages 35–44. Springer, 2016.
3. James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of
constraints using hitting set dualization. In PADL, pages 174–186. Springer, 2005.
4. Jiˇ r´ ı Barnat, Petr Bauch, Nikola Beneˇ s, Luboˇ s Brim, Jan Beran, and Tom´ aˇ s Kratochv´ ıla. Analysing sanity of requirements for avionics systems. FAoC, 2016.
5. Anton Belov and Jo˜ ao Marques-Silva. MUSer2: An efficient MUS extractor. JSAT,
8:123–128, 2012.
6. Jaroslav Bend´ ık. Consistency checking in requirements analysis. In ISSTA, pages
408–411. ACM, 2017.
7. Jaroslav Bend´ ık, Nikola Beneˇ s, Ivana ˇ
Cern´ a, and Jiˇ r´ ı Barnat. Tunable online
MUS/MSS enumeration. In FSTTCS, volume 65 of LIPIcs, pages 50:1–50:13.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
8. Jaroslav Bend´ ık and Ivana ˇ
Cern´ a. Evaluation of domain agnostic approaches for
enumeration of minimal unsatisfiable subsets. In LPAR, volume 57 of EPiC Series
in Computing, pages 131–142. EasyChair, 2018.
9. Jaroslav Bend´ ık, Ivana ˇ
Cern´ a, and Nikola Beneˇ s. Recursive online enumeration of
all minimal unsatisfiable subsets. In ATVA, volume 11138 of LNCS, pages 143–159.
Springer, 2018.
10. Jaroslav Bend´ ık, Elaheh Ghassabani, Michael W. Whalen, and Ivana ˇ
Cern´ a. Online
enumeration of all minimal inductive validity cores. In SEFM, volume 10886 of
LNCS, pages 189–204. Springer, 2018.
11. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta.
The nuxmv symbolic model checker. In CAV, volume 8559 of LNCS, pages 334–342.
Springer, 2014.
12. Huan Chen and Jo˜ ao Marques-Silva. Improvements to satisfiability-based boolean
function bi-decomposition. In VLSI-SoC, pages 142–147. IEEE, 2011.
13. Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Computing small
unsatisfiable cores in satisfiability modulo theories. JAIR, 40:701–728, 2011.
14. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
Counterexample-guided abstraction refinement. In CAV, volume 1855 of LNCS,
pages 154–169. Springer, 2000.
15. Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel, and Vadim
Ryvchin. Designers work less with quality formal equivalence checking. In Design and Verification Conference (DVCon). Citeseer, 2010.
16. Leonardo Mendon¸ ca de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver.
In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008.
17. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud
Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - A framework for LTL
and ω-automata manipulation. In ATVA, volume 9938 of LNCS, pages 122–129,
2016.
18. Niklas E´ en and Niklas S¨ orensson. An extensible SAT-solver. In SAT, volume 2919
of LNCS, pages 502–518. Springer, 2003.