Farkas certificates and minimal witnesses
341
17. Blum, M., Kannan, S.: Designing programs that check their work. Journal of the
ACM 42(1), 269–291 (1995), https://doi.org/10.1145/200836.200880
18. Braitling, B., Wimmer, R., Becker, B., Jansen, N., ´
Abrah´ am, E.: Counterexample
generation for Markov chains using SMT-based bounded model checking. In: Formal
Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FORTE
2011. pp. 75–89 (2011), https://doi.org/10.1007/978-3-642-21461-5 5
19. Br´ azdil, T., Chatterjee, K., Chmelik, M., Fellner, A., Kret´ ınsk´ y, J.: Counterexample
explanation by learning small strategies in Markov decision processes. In: Computer
Aided Verification - 27th International Conference, CAV 2015. pp. 158–177 (2015),
https://doi.org/10.1007/978-3-319-21690-4 10
20. Br´ azdil, T., Chatterjee, K., Chmel´ ık, M., Forejt, V., Kˇ ret´ ınsk´ y, J., Kwiatkowska,
M., Parker, D., Ujma, M.: Verification of Markov Decision Processes Using Learning
Algorithms. In: Automated Technology for Verification and Analysis (ATVA 2014).
pp. 98–114 (2014), https://doi.org/10.1007/978-3-319-11936-6 8
21. Bremner, D., Fukuda, K., Marzetta, A.: Primal–dual methods for vertex and
facet enumeration. Discrete & Computational Geometry 20(3), 333–357 (1998),
https://doi.org/10.1007/PL00009389
22. Bussieck, M.R., L¨ ubbecke, M.E.: The vertex set of a 0/1 polytope is strongly
P-enumerable. Computational Geometry Theory and Applications 11(2), 103–109
(1998)
23. Ceska, M., Hensel, C., Junges, S., Katoen, J.: Counterexample-driven synthesis
for probabilistic program sketches. In: Formal Methods - The Next 30 Years -
Third World Congress, FM 2019. pp. 101–120 (2019), https://doi.org/10.1007/
978-3-030-30942-8 8
24. Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement
framework for Markov decision processes. ACM Transactions on Computational
Logic 12(1), 1:1–1:49 (2010), http://doi.acm.org/10.1145/1838552.1838553
25. Chatterjee, K., Chmelik, M., Daca, P.: CEGAR for qualitative analysis of probabilistic systems. In: Computer Aided Verification - 26th International Conference,
CAV 2014. pp. 473–490 (2014), https://doi.org/10.1007/978-3-319-08867-9 31
26. Ciesinski, F., Baier, C., Gr¨ oßer, M., Klein, J.: Reduction techniques
for model checking Markov decision processes. In: 2008 Fifth International Conference on Quantitative Evaluation of Systems. pp. 45–54 (2008).
https://doi.org/10.1109/QEST.2008.45
27. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided
abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003),
https://doi.org/10.1145/876638.876643
28. Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking.
In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 19–29
(2002), https://doi.org/10.1109/LICS.2002.1029814
29. Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Verification: Theory and Practice, Essays Dedicated to Zohar Manna on
the Occasion of His 64th Birthday. pp. 208–224 (2003), https://doi.org/10.1007/
978-3-540-39910-0 9
30. Col´ on, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using
non-linear constraint solving. In: Computer Aided Verification, 15th International
Conference, CAV 2003. pp. 420–432 (2003)
31. Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state
probabilistic programs. In: Proceedings of the 29th Annual Symposium on Founda-
341
17. Blum, M., Kannan, S.: Designing programs that check their work. Journal of the
ACM 42(1), 269–291 (1995), https://doi.org/10.1145/200836.200880
18. Braitling, B., Wimmer, R., Becker, B., Jansen, N., ´
Abrah´ am, E.: Counterexample
generation for Markov chains using SMT-based bounded model checking. In: Formal
Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FORTE
2011. pp. 75–89 (2011), https://doi.org/10.1007/978-3-642-21461-5 5
19. Br´ azdil, T., Chatterjee, K., Chmelik, M., Fellner, A., Kret´ ınsk´ y, J.: Counterexample
explanation by learning small strategies in Markov decision processes. In: Computer
Aided Verification - 27th International Conference, CAV 2015. pp. 158–177 (2015),
https://doi.org/10.1007/978-3-319-21690-4 10
20. Br´ azdil, T., Chatterjee, K., Chmel´ ık, M., Forejt, V., Kˇ ret´ ınsk´ y, J., Kwiatkowska,
M., Parker, D., Ujma, M.: Verification of Markov Decision Processes Using Learning
Algorithms. In: Automated Technology for Verification and Analysis (ATVA 2014).
pp. 98–114 (2014), https://doi.org/10.1007/978-3-319-11936-6 8
21. Bremner, D., Fukuda, K., Marzetta, A.: Primal–dual methods for vertex and
facet enumeration. Discrete & Computational Geometry 20(3), 333–357 (1998),
https://doi.org/10.1007/PL00009389
22. Bussieck, M.R., L¨ ubbecke, M.E.: The vertex set of a 0/1 polytope is strongly
P-enumerable. Computational Geometry Theory and Applications 11(2), 103–109
(1998)
23. Ceska, M., Hensel, C., Junges, S., Katoen, J.: Counterexample-driven synthesis
for probabilistic program sketches. In: Formal Methods - The Next 30 Years -
Third World Congress, FM 2019. pp. 101–120 (2019), https://doi.org/10.1007/
978-3-030-30942-8 8
24. Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement
framework for Markov decision processes. ACM Transactions on Computational
Logic 12(1), 1:1–1:49 (2010), http://doi.acm.org/10.1145/1838552.1838553
25. Chatterjee, K., Chmelik, M., Daca, P.: CEGAR for qualitative analysis of probabilistic systems. In: Computer Aided Verification - 26th International Conference,
CAV 2014. pp. 473–490 (2014), https://doi.org/10.1007/978-3-319-08867-9 31
26. Ciesinski, F., Baier, C., Gr¨ oßer, M., Klein, J.: Reduction techniques
for model checking Markov decision processes. In: 2008 Fifth International Conference on Quantitative Evaluation of Systems. pp. 45–54 (2008).
https://doi.org/10.1109/QEST.2008.45
27. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided
abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003),
https://doi.org/10.1145/876638.876643
28. Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking.
In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 19–29
(2002), https://doi.org/10.1109/LICS.2002.1029814
29. Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Verification: Theory and Practice, Essays Dedicated to Zohar Manna on
the Occasion of His 64th Birthday. pp. 208–224 (2003), https://doi.org/10.1007/
978-3-540-39910-0 9
30. Col´ on, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using
non-linear constraint solving. In: Computer Aided Verification, 15th International
Conference, CAV 2003. pp. 420–432 (2003)
31. Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state
probabilistic programs. In: Proceedings of the 29th Annual Symposium on Founda-