Chatterjee, K., Henzinger, T. A., Otop, J., &; Velner, Y. (2017). Quantitative fair simulation games. Information and Computation. Elsevier.https://doi.org/10.1016/j.ic.2016.10.006 
LibreCat: https://research-explorer.ista.ac.at/record/1066
DOI: 10.1016/j.ic.2016.10.006
WoS: 000402025600002

Chatterjee, K., Kragl, B., Mishra, S., &; Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer.https://doi.org/10.1007/978-3-662-54434-1_11 
LibreCat: https://research-explorer.ista.ac.at/record/1011
DOI: 10.1007/978-3-662-54434-1_11
WoS: 000681702400011

Avni, G., Guha, S., &; Kupferman, O. (2017). An abstraction-refinement methodology for reasoning about network games (pp. 70–76). Presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia: AAAI Press.https://doi.org/10.24963/ijcai.2017/11 
LibreCat: https://research-explorer.ista.ac.at/record/1003
DOI: 10.24963/ijcai.2017/11
WoS: 000764137500011

Trinh, M., Chu, D. H., &; Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar &; V. Kundak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer.https://doi.org/10.1007/978-3-319-63390-9_21 
LibreCat: https://research-explorer.ista.ac.at/record/962
DOI: 10.1007/978-3-319-63390-9_21
WoS: 000431900900021

Le, X., Chu, D. H., Lo, D., Le Goues, C., &; Visser, W. (2017). : Syntax- and semantic-guided repair synthesis via programming by examples (Vol. 0154, pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn, Germany: ACM.https://doi.org/10.1145/3106237.3106309 
LibreCat: https://research-explorer.ista.ac.at/record/942
DOI: 10.1145/3106237.3106309
WoS: 000414279300055

Gottlob, G., Henzinger, T. A., &; Weißenbacher, G. (2017). Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. Springer.https://doi.org/10.1007/s10703-017-0307-6 
LibreCat: https://research-explorer.ista.ac.at/record/743
DOI: 10.1007/s10703-017-0307-6
WoS: 000415615600001

Finkbeiner, B., &; Kupriyanov, A. (2017). Causality-based model checking. In Electronic Proceedings in Theoretical Computer Science (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association.https://doi.org/10.4204/EPTCS.259.3 
LibreCat: https://research-explorer.ista.ac.at/record/549
DOI: 10.4204/EPTCS.259.3

Chatterjee, K., Henzinger, T. A., &; Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.4230/LIPIcs.MFCS.2016.24 
LibreCat: https://research-explorer.ista.ac.at/record/1090
DOI: 10.4230/LIPIcs.MFCS.2016.24

Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H.,https://doi.org/10.4230/LIPIcs.CONCUR.2016.6__Veith, H. (2016). Local linearizability for concurrent container-type data structures. In Leibniz International Proceedings in Informatics (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.4230/LIPIcs.CONCUR.2016.6 
LibreCat: https://research-explorer.ista.ac.at/record/1095
DOI: 10.4230/LIPIcs.CONCUR.2016.6

Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., &; Ray, R. (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE.https://doi.org/10.1109/MEMCOD.2016.7797741 
LibreCat: https://research-explorer.ista.ac.at/record/1103
DOI: 10.1109/MEMCOD.2016.7797741

Avni, G., Guha, S., &; Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In Proceedings of the 13th International Conference on Embedded Software . Pittsburgh, PA, USA: ACM.https://doi.org/10.1145/2968478.2968499 
LibreCat: https://research-explorer.ista.ac.at/record/1135
DOI: 10.1145/2968478.2968499

Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M.,https://doi.org/10.1109/CCA.2016.7587948__Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesishttps://doi.org/10.1109/CCA.2016.7587948__HyST and TuLiP. In 2016 IEEE Conference on Control Applications. Buenos Aires, Argentina : IEEE.https://doi.org/10.1109/CCA.2016.7587948 
LibreCat: https://research-explorer.ista.ac.at/record/1134
DOI: 10.1109/CCA.2016.7587948

Chatterjee, K., Henzinger, T. A., &; Otop, J. (2016). Quantitative automata under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium (pp. 76–85). New York, NY, USA: IEEE.https://doi.org/10.1145/2933575.2933588 
LibreCat: https://research-explorer.ista.ac.at/record/1138
DOI: 10.1145/2933575.2933588
arXiv: 1604.06764

Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., &; Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer.https://doi.org/10.1007/978-3-319-47151-8_9 
LibreCat: https://research-explorer.ista.ac.at/record/1227
DOI: 10.1007/978-3-319-47151-8_9

Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., &; Sha, L. (2016). From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria: IEEE.https://doi.org/10.1109/RTAS.2016.7461337 
LibreCat: https://research-explorer.ista.ac.at/record/1256
DOI: 10.1109/RTAS.2016.7461337

Chatterjee, K., Henzinger, T. A., &; Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer.https://doi.org/10.1007/978-3-662-53413-7_2 
LibreCat: https://research-explorer.ista.ac.at/record/1335
DOI: 10.1007/978-3-662-53413-7_2

D’Antoni, L., Samanta, R., &; Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer.https://doi.org/10.1007/978-3-319-41540-6_21 
LibreCat: https://research-explorer.ista.ac.at/record/1390
DOI: 10.1007/978-3-319-41540-6_21

Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., &; Prakash, P. (2016). Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164). Presented at the HSCC 2016: International Conference on Hybrid Systems: Computation and Control, Vienna, Austria: Springer.https://doi.org/10.1145/2883817.2883837 
LibreCat: https://research-explorer.ista.ac.at/record/1421
DOI: 10.1145/2883817.2883837

Dragoi, C., Henzinger, T. A., &; Zufferey, D. (2016). PSYNC: A partially synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp. 400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM.https://doi.org/10.1145/2837614.2837650 
LibreCat: https://research-explorer.ista.ac.at/record/1439
DOI: 10.1145/2837614.2837650

Beica, A., Guet, C. C., &; Petrov, T. (2016). Efficient reduction of kappa models by static inspection of the rule-set (Vol. 9271, pp. 173–191). Presented at the HSB: Hybrid Systems Biology, Madrid, Spain: Springer.https://doi.org/10.1007/978-3-319-26916-0_10 
LibreCat: https://research-explorer.ista.ac.at/record/1524
DOI: 10.1007/978-3-319-26916-0_10

Henzinger, T. A., Otop, J., &; Samanta, R. (2016). Lipschitz robustness of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer.https://doi.org/10.1007/978-3-662-49122-5_12 
LibreCat: https://research-explorer.ista.ac.at/record/1526
DOI: 10.1007/978-3-662-49122-5_12

Schilling, C., Bogomolov, S., Henzinger, T. A., Podelski, A., &; Ruess, J. (2016). Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. Elsevier.https://doi.org/10.1016/j.biosystems.2016.07.005 
LibreCat: https://research-explorer.ista.ac.at/record/1148
DOI: 10.1016/j.biosystems.2016.07.005

Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H.,https://doi.org/10.1007/s10009-015-0393-y__Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space abstractions. International Journal on Software Tools for Technology Transfer. Springer.https://doi.org/10.1007/s10009-015-0393-y 
LibreCat: https://research-explorer.ista.ac.at/record/1705
DOI: 10.1007/s10009-015-0393-y

Jiang, Y., Liu, H., Kong, H., Wang, R., Hosseini, M., Sun, J., &; Sha, L. (2016). Use runtime verification to improve the quality of medical care practice. In Proceedings of the 38th International Conference on Software Engineering Companion  (pp. 112–121). Austin, TX, USA: IEEE.https://doi.org/10.1145/2889160.2889233 
LibreCat: https://research-explorer.ista.ac.at/record/479
DOI: 10.1145/2889160.2889233

Chatterjee, K., Chmelik, M., &; Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press.
LibreCat: https://research-explorer.ista.ac.at/record/1166

Avni, G., Henzinger, T. A., &; Kupferman, O. (2016). Dynamic resource allocation games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer.https://doi.org/10.1007/978-3-662-53354-3_13 
LibreCat: https://research-explorer.ista.ac.at/record/1341
DOI: 10.1007/978-3-662-53354-3_13

Tarrach, T. (2016). Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria.https://doi.org/10.15479/at:ista:1130 
LibreCat: https://research-explorer.ista.ac.at/record/1130
DOI: 10.15479/at:ista:1130

Daca, P., Henzinger, T. A., Kretinsky, J., &; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.4230/LIPIcs.CONCUR.2016.20 
LibreCat: https://research-explorer.ista.ac.at/record/1093
DOI: 10.4230/LIPIcs.CONCUR.2016.20

Daca, P., Henzinger, T. A., Kretinsky, J., &; Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer.https://doi.org/10.1007/978-3-662-49674-9_7 
LibreCat: https://research-explorer.ista.ac.at/record/1234
DOI: 10.1007/978-3-662-49674-9_7

Daca, P., Gupta, A., &; Henzinger, T. A. (2016). Abstraction-driven concolic testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer.https://doi.org/10.1007/978-3-662-49122-5_16 
LibreCat: https://research-explorer.ista.ac.at/record/1230
DOI: 10.1007/978-3-662-49122-5_16

Daca, P., Henzinger, T. A., &; Kupriyanov, A. (2016). Array folds logic (Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer.https://doi.org/10.1007/978-3-319-41540-6_13 
LibreCat: https://research-explorer.ista.ac.at/record/1391
DOI: 10.1007/978-3-319-41540-6_13

Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., &; Sha, L. (2016). Safety assured formal model driven design of the multifunction vehicle bus controller (Vol. 9995, pp. 757–763). Presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus: Springer.https://doi.org/10.1007/978-3-319-48989-6_47 
LibreCat: https://research-explorer.ista.ac.at/record/1205
DOI: 10.1007/978-3-319-48989-6_47

Parise, F., Lygeros, J., &; Ruess, J. (2015). Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. Frontiers in Environmental Science. Frontiers.https://doi.org/10.3389/fenvs.2015.00042 
LibreCat: https://research-explorer.ista.ac.at/record/10794
DOI: 10.3389/fenvs.2015.00042

Dragoi, C., Henzinger, T. A., &; Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.4230/LIPIcs.SNAPL.2015.90 
LibreCat: https://research-explorer.ista.ac.at/record/1498
DOI: 10.4230/LIPIcs.SNAPL.2015.90

Kretinsky, J., Larsen, K., Laursen, S., &; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.4230/LIPIcs.CONCUR.2015.142 
LibreCat: https://research-explorer.ista.ac.at/record/1499
DOI: 10.4230/LIPIcs.CONCUR.2015.142

Ruess, J. (2015). Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. Journal of Chemical Physics. American Institute of Physics.https://doi.org/10.1063/1.4937937 
LibreCat: https://research-explorer.ista.ac.at/record/1539
DOI: 10.1063/1.4937937

Ruess, J., Parise, F., Milias Argeitis, A., Khammash, M., &; Lygeros, J. (2015). Iterative experiment design guides the characterization of a light-inducible gene expression circuit. PNAS. National Academy of Sciences.https://doi.org/10.1073/pnas.1423947112 
LibreCat: https://research-explorer.ista.ac.at/record/1538
DOI: 10.1073/pnas.1423947112
PMID: 26085136

Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., &; Grosu, R. (2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer.https://doi.org/10.1007/978-3-319-26287-1_1 
LibreCat: https://research-explorer.ista.ac.at/record/1541
DOI: 10.1007/978-3-319-26287-1_1

Forejt, V., Krdál, J., &; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\'47U (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer.https://doi.org/10.1007/978-3-662-48899-7_12 
LibreCat: https://research-explorer.ista.ac.at/record/1594
DOI: 10.1007/978-3-662-48899-7_12

Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D.,https://doi.org/10.1007/978-3-319-21690-4_31__Strejdek, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer.https://doi.org/10.1007/978-3-319-21690-4_31 
LibreCat: https://research-explorer.ista.ac.at/record/1601
DOI: 10.1007/978-3-319-21690-4_31

Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., &; Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer.https://doi.org/10.1007/978-3-319-26287-1_2 
LibreCat: https://research-explorer.ista.ac.at/record/1605
DOI: 10.1007/978-3-319-26287-1_2

Nguyen, L., Schilling, C., Bogomolov, S., &; Johnson, T. (2015). Runtime verification for hybrid analysis tools. In 6th International Conference (Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature.https://doi.org/10.1007/978-3-319-23820-3_19 
LibreCat: https://research-explorer.ista.ac.at/record/1606
DOI: 10.1007/978-3-319-23820-3_19

Bogomolov, S., Henzinger, T. A., Podelski, A., Ruess, J., &; Schilling, C. (2015). Adaptive moment closure for parameter inference of biochemical reaction networks. Presented at the CMSB: Computational Methods in Systems Biology, Nantes, France: Springer.https://doi.org/10.1007/978-3-319-23401-4_8 
LibreCat: https://research-explorer.ista.ac.at/record/1658
DOI: 10.1007/978-3-319-23401-4_8

Bogomolov, S., Magazzeni, D., Minopoli, S., &; Wehrle, M. (2015). PDDL+ planning with hybrid automata: Foundations of translating must behavior (pp. 42–46). Presented at the ICAPS: International Conference on Automated Planning and Scheduling, Jerusalem, Israel: AAAI Press.
LibreCat: https://research-explorer.ista.ac.at/record/1670

Michaliszyn, J., Otop, J., &; Kieroski, E. (2015). On the decidability of elementary modal logics. ACM Transactions on Computational Logic. ACM.https://doi.org/10.1145/2817825 
LibreCat: https://research-explorer.ista.ac.at/record/1680
DOI: 10.1145/2817825

Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., &; Podelski, A. (2015). Eliminating spurious transitions in reachability with support functions. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 149–158). Seattle, WA, United States: ACM.https://doi.org/10.1145/2728606.2728622 
LibreCat: https://research-explorer.ista.ac.at/record/1692
DOI: 10.1145/2728606.2728622

Bak, S., Bogomolov, S., &; Johnson, T. (2015). HYST: A source transformation and translation tool for hybrid automaton models (pp. 128–133). Presented at the HSCC: Hybrid Systems - Computation and Control, Seattle, WA, United States: Springer.https://doi.org/10.1145/2728606.2728630 
LibreCat: https://research-explorer.ista.ac.at/record/1690
DOI: 10.1145/2728606.2728630

Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &; Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. Information and Computation. Elsevier.https://doi.org/10.1016/j.ic.2015.03.001 
LibreCat: https://research-explorer.ista.ac.at/record/1698
DOI: 10.1016/j.ic.2015.03.001

Gupta, A., &; Henzinger, T. A. (2015). Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. ACM.https://doi.org/10.1145/2745799 
LibreCat: https://research-explorer.ista.ac.at/record/1808
DOI: 10.1145/2745799

Cerny, P., Henzinger, T. A., Kovács, L., Radhakrishna, A., &; Zwirchmayr, J. (2015). Segment abstraction for worst-case execution time analysis. Presented at the ESOP: European Symposium on Programming, London, United Kingdom: Springer.https://doi.org/10.1007/978-3-662-46669-8_5 
LibreCat: https://research-explorer.ista.ac.at/record/1836
DOI: 10.1007/978-3-662-46669-8_5

Benes, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., &; Srba, J. (2015). Refinement checking on parametric modal transition systems. Acta Informatica. Springer.https://doi.org/10.1007/s00236-015-0215-4 
LibreCat: https://research-explorer.ista.ac.at/record/1846
DOI: 10.1007/s00236-015-0215-4

Geiger, B., Petrov, T., Kubin, G., &; Koeppl, H. (2015). Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. IEEE.https://doi.org/10.1109/TAC.2014.2364971 
LibreCat: https://research-explorer.ista.ac.at/record/1840
DOI: 10.1109/TAC.2014.2364971

Ruess, J., &; Lygeros, J. (2015). Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. ACM Transactions on Modeling and Computer Simulation. ACM.https://doi.org/10.1145/2688906 
LibreCat: https://research-explorer.ista.ac.at/record/1861
DOI: 10.1145/2688906

Henzinger, T. A., &; Raskin, J. (2015). The equivalence problem for finite automata: Technical perspective. Communications of the ACM. ACM.https://doi.org/10.1145/2701001 
LibreCat: https://research-explorer.ista.ac.at/record/1866
DOI: 10.1145/2701001

Fahrenberg, U., Kretinsky, J., Legay, A., &; Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer.https://doi.org/10.1007/978-3-319-15317-9_19 
LibreCat: https://research-explorer.ista.ac.at/record/1882
DOI: 10.1007/978-3-319-15317-9_19

Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM.https://doi.org/10.1145/2676726.2677008 
LibreCat: https://research-explorer.ista.ac.at/record/1992
DOI: 10.1145/2676726.2677008

Chakraborty, S., Henzinger, T. A., Sezgin, A., &; Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. Logical Methods in Computer Science. International Federation of Computational Logic.https://doi.org/10.2168/LMCS-11(1:20)2015 
LibreCat: https://research-explorer.ista.ac.at/record/1832
DOI: 10.2168/LMCS-11(1:20)2015

Chatterjee, K., Doyen, L., Gimbert, H., &; Henzinger, T. A. (2015). Randomness for free. Information and Computation. Elsevier.https://doi.org/10.1016/j.ic.2015.06.003 
LibreCat: https://research-explorer.ista.ac.at/record/1731
DOI: 10.1016/j.ic.2015.06.003

Chatterjee, K., Henzinger, T. A., Jobstmann, B., &; Singh, R. (2015). Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. ACM.https://doi.org/10.1145/2699430 
LibreCat: https://research-explorer.ista.ac.at/record/1856
DOI: 10.1145/2699430

Chatterjee, K., Komárková, Z., &; Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE.https://doi.org/10.1109/LICS.2015.32 
LibreCat: https://research-explorer.ista.ac.at/record/1657
DOI: 10.1109/LICS.2015.32

Chatterjee, K., Henzinger, T. A., &; Otop, J. (2015). Nested weighted automata. In Proceedings - Symposium on Logic in Computer Science (Vol. 2015–July). Kyoto, Japan: IEEE.https://doi.org/10.1109/LICS.2015.72 
LibreCat: https://research-explorer.ista.ac.at/record/1656
DOI: 10.1109/LICS.2015.72
arXiv: 1606.03598

Chatterjee, K., Henzinger, T. A., &; Otop, J. (2015). Nested weighted automata. IST Austria.https://doi.org/10.15479/AT:IST-2015-170-v2-2 
LibreCat: https://research-explorer.ista.ac.at/record/5436
DOI: 10.15479/AT:IST-2015-170-v2-2

Boker, U., Henzinger, T. A., &; Otop, J. (2015). The target discounted-sum problem. In LICS (pp. 750–761). Kyoto, Japan: IEEE.https://doi.org/10.1109/LICS.2015.74 
LibreCat: https://research-explorer.ista.ac.at/record/1659
DOI: 10.1109/LICS.2015.74

Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &; Otop, J. (2015). Edit distance for pushdown automata. In 42nd International Colloquium (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature.https://doi.org/10.1007/978-3-662-47666-6_10 
LibreCat: https://research-explorer.ista.ac.at/record/1610
DOI: 10.1007/978-3-662-47666-6_10
arXiv: 1504.08259

Boker, U., Henzinger, T. A., &; Otop, J. (2015). The target discounted-sum problem. IST Austria.https://doi.org/10.15479/AT:IST-2015-335-v1-1 
LibreCat: https://research-explorer.ista.ac.at/record/5439
DOI: 10.15479/AT:IST-2015-335-v1-1

Benes, N., Daca, P., Henzinger, T. A., Kretinsky, J., &; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM.https://doi.org/10.1145/2737166.2737175 
LibreCat: https://research-explorer.ista.ac.at/record/1502
DOI: 10.1145/2737166.2737175

Chatterjee, K., Chmelik, M., &; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. Springer.https://doi.org/10.1007/s10703-015-0235-2 
LibreCat: https://research-explorer.ista.ac.at/record/1501
DOI: 10.1007/s10703-015-0235-2

Svoreová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cbrná, I., &; Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle, WA, United States: ACM.https://doi.org/10.1145/2728606.2728608 
LibreCat: https://research-explorer.ista.ac.at/record/1689
DOI: 10.1145/2728606.2728608

Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &; Tarrach, T. (2015). From non-preemptive to preemptive scheduling using synchronization synthesis. Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer.https://doi.org/10.1007/978-3-319-21668-3_11 
LibreCat: https://research-explorer.ista.ac.at/record/1729
DOI: 10.1007/978-3-319-21668-3_11

Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &; Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer.https://doi.org/10.1007/978-3-662-46681-0_47 
LibreCat: https://research-explorer.ista.ac.at/record/1835
DOI: 10.1007/978-3-662-46681-0_47

Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &; Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer.https://doi.org/10.1007/978-3-319-21690-4_10 
LibreCat: https://research-explorer.ista.ac.at/record/1603
DOI: 10.1007/978-3-319-21690-4_10

Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria.https://doi.org/10.15479/AT:ISTA:28 
LibreCat: https://research-explorer.ista.ac.at/record/5549
DOI: 10.15479/AT:ISTA:28

Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., &; Zufferey, D. (2014). A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA: Springer.https://doi.org/10.1007/978-3-642-54013-4_10 
LibreCat: https://research-explorer.ista.ac.at/record/1392
DOI: 10.1007/978-3-642-54013-4_10

Gordon, A., Henzinger, T. A., Nori, A., &; Rajamani, S. (2014). Probabilistic programming. In Proceedings of the on Future of Software Engineering (pp. 167–181). Hyderabad, India: ACM.https://doi.org/10.1145/2593882.2593900 
LibreCat: https://research-explorer.ista.ac.at/record/1393
DOI: 10.1145/2593882.2593900

Gupta, A., Popeea, C., &; Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing.https://doi.org/10.4204/EPTCS.169.5 
LibreCat: https://research-explorer.ista.ac.at/record/1702
DOI: 10.4204/EPTCS.169.5

Hofferek, G., &; Gupta, A. (2014). Suraq - a controller synthesis tool using uninterpreted functions. In E. Yahav (Ed.), HVC 2014 (Vol. 8855, pp. 68–74). Haifa, Israel: Springer.https://doi.org/10.1007/978-3-319-13338-6_6 
LibreCat: https://research-explorer.ista.ac.at/record/1869
DOI: 10.1007/978-3-319-13338-6_6

Gupta, A., Kovács, L., Kragl, B., &; Voronkov, A. (2014). Extensional crisis and proving identity. In F. Cassez &; J.-F. Raskin (Eds.), ATVA 2014 (Vol. 8837, pp. 185–200). Sydney, Australia: Springer.https://doi.org/10.1007/978-3-319-11936-6_14 
LibreCat: https://research-explorer.ista.ac.at/record/1872
DOI: 10.1007/978-3-319-11936-6_14

Henzinger, T. A., Otop, J., &; Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In Leibniz International Proceedings in Informatics, LIPIcs (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431 
LibreCat: https://research-explorer.ista.ac.at/record/1870
DOI: 10.4230/LIPIcs.FSTTCS.2014.431

Samanta, R., Olivo, O., &; Allen, E. (2014). Cost-aware automatic program repair. In M. Müller-Olm &; H. Seidl (Eds.) (Vol. 8723, pp. 268–284). Presented at the SAS: Static Analysis Symposium, Munich, Germany: Springer.https://doi.org/10.1007/978-3-319-10936-7_17 
LibreCat: https://research-explorer.ista.ac.at/record/1875
DOI: 10.1007/978-3-319-10936-7_17

Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M.,https://doi.org/10.1007/978-3-319-11936-6_8__Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez &; J.-F. Raskin (Eds.), https://doi.org/10.1007/978-3-319-11936-6_8__Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics.https://doi.org/10.1007/978-3-319-11936-6_8 
LibreCat: https://research-explorer.ista.ac.at/record/2027
DOI: 10.1007/978-3-319-11936-6_8

Komárková, Z., &; Kretinsky, J. (2014). Rabinizer 3: Safraless translation of ltl to small deterministic automata. In F. Cassez &; J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 235–241). Sydney, Australia: Springer.https://doi.org/10.1007/978-3-319-11936-6_17 
LibreCat: https://research-explorer.ista.ac.at/record/2026
DOI: 10.1007/978-3-319-11936-6_17

Hermanns, H., Krdál, J., &; Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan &; D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.https://doi.org/10.1007/978-3-662-44584-6_18 
LibreCat: https://research-explorer.ista.ac.at/record/2053
DOI: 10.1007/978-3-662-44584-6_18

Ganguly, A., Petrov, T., &; Koeppl, H. (2014). Markov chain aggregation and its applications to combinatorial reaction networks. Journal of Mathematical Biology. Springer.https://doi.org/10.1007/s00285-013-0738-7 
LibreCat: https://research-explorer.ista.ac.at/record/2056
DOI: 10.1007/s00285-013-0738-7

Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., Hofferek, G., Jobstmann, B.,https://doi.org/10.1007/s00236-013-0191-5__Könighofer, R. (2014). Synthesizing robust systems. Acta Informatica. Springer.https://doi.org/10.1007/s00236-013-0191-5 
LibreCat: https://research-explorer.ista.ac.at/record/2187
DOI: 10.1007/s00236-013-0191-5

Esparza, J., &; Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer.https://doi.org/10.1007/978-3-319-08867-9_13 
LibreCat: https://research-explorer.ista.ac.at/record/2190
DOI: 10.1007/978-3-319-08867-9_13

Boker, U., &; Henzinger, T. A. (2014). Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. International Federation of Computational Logic.https://doi.org/10.2168/LMCS-10(1:10)2014 
LibreCat: https://research-explorer.ista.ac.at/record/2233
DOI: 10.2168/LMCS-10(1:10)2014

Boker, U., Henzinger, T. A., &; Radhakrishna, A. (2014). Battery transition systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming Languages, San Diego, USA: ACM.https://doi.org/10.1145/2535838.2535875 
LibreCat: https://research-explorer.ista.ac.at/record/2239
DOI: 10.1145/2535838.2535875

Cerny, P., Chmelik, M., Henzinger, T. A., &; Radhakrishna, A. (2014). Interface simulation distances. Theoretical Computer Science. Elsevier.https://doi.org/10.1016/j.tcs.2014.08.019 
LibreCat: https://research-explorer.ista.ac.at/record/1733
DOI: 10.1016/j.tcs.2014.08.019

Boker, U., Chatterjee, K., Henzinger, T. A., &; Kupferman, O. (2014). Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). ACM.https://doi.org/10.1145/2629686 
LibreCat: https://research-explorer.ista.ac.at/record/2038
DOI: 10.1145/2629686

Daca, P., Henzinger, T. A., Krenn, W., &; Nickovic, D. (2014). Compositional specifications for IOCO testing. IST Austria.https://doi.org/10.15479/AT:IST-2014-148-v2-1 
LibreCat: https://research-explorer.ista.ac.at/record/5411
DOI: 10.15479/AT:IST-2014-148-v2-1

Henzinger, T. A., &; Otop, J. (2014). Model measuring for hybrid systems. In Proceedings of the 17th international conference on Hybrid systems: computation and control (pp. 213–222). Berlin, Germany: Springer.https://doi.org/10.1145/2562059.2562130 
LibreCat: https://research-explorer.ista.ac.at/record/2217
DOI: 10.1145/2562059.2562130

Henzinger, T. A., &; Otop, J. (2014). From model checking to model measuring. IST Austria.https://doi.org/10.15479/AT:IST-2014-172-v1-1 
LibreCat: https://research-explorer.ista.ac.at/record/5417
DOI: 10.15479/AT:IST-2014-172-v1-1

Henzinger, T. A., &; Otop, J. (2014). Model measuring for hybrid systems. IST Austria.https://doi.org/10.15479/AT:IST-2014-171-v1-1 
LibreCat: https://research-explorer.ista.ac.at/record/5416
DOI: 10.15479/AT:IST-2014-171-v1-1

Chatterjee, K., Henzinger, T. A., &; Otop, J. (2014). Nested weighted automata. IST Austria.https://doi.org/10.15479/AT:IST-2014-170-v1-1 
LibreCat: https://research-explorer.ista.ac.at/record/5415
DOI: 10.15479/AT:IST-2014-170-v1-1

Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., &; Tarrach, T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer.https://doi.org/10.1007/978-3-319-08867-9_38 
LibreCat: https://research-explorer.ista.ac.at/record/2218
DOI: 10.1007/978-3-319-08867-9_38

Daca, P., Henzinger, T. A., Krenn, W., &; Nickovic, D. (2014). Compositional specifications for IOCO testing. In IEEE 7th International Conference on Software Testing, Verification and Validation. Cleveland, USA: IEEE.https://doi.org/10.1109/ICST.2014.50 
LibreCat: https://research-explorer.ista.ac.at/record/2167
DOI: 10.1109/ICST.2014.50
arXiv: 1904.07083

Chatterjee, K., Chmelik, M., &; Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer.https://doi.org/10.1007/978-3-319-08867-9_31 
LibreCat: https://research-explorer.ista.ac.at/record/2063
DOI: 10.1007/978-3-319-08867-9_31

Chatterjee, K., Henzinger, T. A., Otop, J., &; Velner, Y. (2014). Quantitative fair simulation games. IST Austria.https://doi.org/10.15479/AT:IST-2014-315-v1-1 
LibreCat: https://research-explorer.ista.ac.at/record/5428
DOI: 10.15479/AT:IST-2014-315-v1-1

Haas, A., Lippautz, M., Henzinger, T. A., Payer, H., Sokolova, A., Kirsch, C. M., &; Sezgin, A. (2013). Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. In Proceedings of the ACM International Conference on Computing Frontiers - CF ’13. Ischia, Italy: ACM Press.https://doi.org/10.1145/2482767.2482789 
LibreCat: https://research-explorer.ista.ac.at/record/10898
DOI: 10.1145/2482767.2482789

Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., &; Bloem, R. (2013). Synthesizing multiple boolean functions using interpolation on a single proof. In 2013 Formal Methods in Computer-Aided Design (pp. 77–84). Portland, OR, United States: IEEE.https://doi.org/10.1109/FMCAD.2013.6679394 
LibreCat: https://research-explorer.ista.ac.at/record/1385
DOI: 10.1109/FMCAD.2013.6679394
arXiv: 1308.4767