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

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

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

Unifying two views on multiple mean-payoff objectives in Markov decision processes
K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.
LibreCat: https://research-explorer.ista.ac.at/record/1657
DOI: 10.1109/LICS.2015.32

Nested weighted automata
K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.
LibreCat: https://research-explorer.ista.ac.at/record/1656
DOI: 10.1109/LICS.2015.72
arXiv: 1606.03598

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

The target discounted-sum problem
U. Boker, T.A. Henzinger, J. Otop, in:, LICS, IEEE, 2015, pp. 750–761.
LibreCat: https://research-explorer.ista.ac.at/record/1659
DOI: 10.1109/LICS.2015.74

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

The target discounted-sum problem
U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST Austria, 2015.
LibreCat: https://research-explorer.ista.ac.at/record/5439
DOI: 10.15479/AT:IST-2015-335-v1-1

Complete composition operators for IOCO-testing theory
N. Benes, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.
LibreCat: https://research-explorer.ista.ac.at/record/1502
DOI: 10.1145/2737166.2737175

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

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

From non-preemptive to preemptive scheduling using synchronization synthesis
P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, 9207 (2015) 180–197.
LibreCat: https://research-explorer.ista.ac.at/record/1729
DOI: 10.1007/978-3-319-21668-3_11

Model checking gene regulatory networks
M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483.
LibreCat: https://research-explorer.ista.ac.at/record/1835
DOI: 10.1007/978-3-662-46681-0_47

Counterexample explanation by learning small strategies in Markov decision processes
T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.
LibreCat: https://research-explorer.ista.ac.at/record/1603
DOI: 10.1007/978-3-319-21690-4_10

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

A logic-based framework for verifying consensus algorithms
C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181.
LibreCat: https://research-explorer.ista.ac.at/record/1392
DOI: 10.1007/978-3-642-54013-4_10

Probabilistic programming
A. Gordon, T.A. Henzinger, A. Nori, S. Rajamani, in:, Proceedings of the on Future of Software Engineering, ACM, 2014, pp. 167–181.
LibreCat: https://research-explorer.ista.ac.at/record/1393
DOI: 10.1145/2593882.2593900

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

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