From LTL to deterministic automata: A safraless compositional approach
J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208.

Exact and approximate determinization of discounted-sum automata
U. Boker, T.A. Henzinger, Logical Methods in Computer Science 10 (2014).

Battery transition systems
U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.

Interface simulation distances
P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.

Temporal specifications with accumulative values
U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014).

Compositional specifications for IOCO testing
P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014.

Model measuring for hybrid systems
T.A. Henzinger, J. Otop, in:, Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, Springer, 2014, pp. 213–222.

From model checking to model measuring
T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria, 2014.

Model measuring for hybrid systems
T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014.

Nested weighted automata
K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014.

Regression-free synthesis for concurrency
P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2014, pp. 568–584.

Compositional specifications for IOCO testing
P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International Conference on Software Testing, Verification and Validation, IEEE, 2014.

CEGAR for qualitative analysis of probabilistic systems
K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.

Quantitative fair simulation games
K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014.

Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation
A. Haas, M. Lippautz, T.A. Henzinger, H. Payer, A. Sokolova, C.M. Kirsch, A. Sezgin, in:, Proceedings of the ACM International Conference on Computing Frontiers - CF ’13, ACM Press, 2013.

Synthesizing multiple boolean functions using interpolation on a single proof
G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.

Nondeterminism in the presence of a diverse or unknown future
U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.

Quantitative relaxation of concurrent data structures
T.A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, A. Sokolova, in:, Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, ACM, 2013, pp. 317–328.

Quantitative abstraction refinement
P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, ACM, 2013, pp. 115–128.

Tree interpolation in Vampire
R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.