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

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

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

Cost-aware automatic program repair
R. Samanta, O. Olivo, E. Allen, in:, M. Müller-Olm, H. Seidl (Eds.), Springer, 2014, pp. 268–284.
LibreCat: https://research-explorer.ista.ac.at/record/1875
DOI: 10.1007/978-3-319-10936-7_17

Verification of markov decision processes using learning algorithms
T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.),  Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114.
LibreCat: https://research-explorer.ista.ac.at/record/2027
DOI: 10.1007/978-3-319-11936-6_8

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

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

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

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

From LTL to deterministic automata: A safraless compositional approach
J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208.
LibreCat: https://research-explorer.ista.ac.at/record/2190
DOI: 10.1007/978-3-319-08867-9_13

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

Battery transition systems
U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.
LibreCat: https://research-explorer.ista.ac.at/record/2239
DOI: 10.1145/2535838.2535875

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

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

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

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.
LibreCat: https://research-explorer.ista.ac.at/record/2217
DOI: 10.1145/2562059.2562130

From model checking to model measuring
T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria, 2014.
LibreCat: https://research-explorer.ista.ac.at/record/5417
DOI: 10.15479/AT:IST-2014-172-v1-1

Model measuring for hybrid systems
T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014.
LibreCat: https://research-explorer.ista.ac.at/record/5416
DOI: 10.15479/AT:IST-2014-171-v1-1

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

Regression-free synthesis for concurrency
P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2014, pp. 568–584.
LibreCat: https://research-explorer.ista.ac.at/record/2218
DOI: 10.1007/978-3-319-08867-9_38

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.
LibreCat: https://research-explorer.ista.ac.at/record/2167
DOI: 10.1109/ICST.2014.50
arXiv: 1904.07083

CEGAR for qualitative analysis of probabilistic systems
K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.
LibreCat: https://research-explorer.ista.ac.at/record/2063
DOI: 10.1007/978-3-319-08867-9_31

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

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.
LibreCat: https://research-explorer.ista.ac.at/record/10898
DOI: 10.1145/2482767.2482789

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.
LibreCat: https://research-explorer.ista.ac.at/record/1385
DOI: 10.1109/FMCAD.2013.6679394
arXiv: 1308.4767

Nondeterminism in the presence of a diverse or unknown future
U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.
LibreCat: https://research-explorer.ista.ac.at/record/1387
DOI: 10.1007/978-3-642-39212-2_11

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.
LibreCat: https://research-explorer.ista.ac.at/record/2181
DOI: 10.1145/2429069.2429109

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.
LibreCat: https://research-explorer.ista.ac.at/record/2182
DOI: 10.1145/2429069.2429085

Tree interpolation in Vampire
R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.
LibreCat: https://research-explorer.ista.ac.at/record/2237
DOI: 10.1007/978-3-642-45221-5_13

Elementary modal logics over transitive structures
J. Michaliszyn, J. Otop, 23 (2013) 563–577.
LibreCat: https://research-explorer.ista.ac.at/record/2243
DOI: 10.4230/LIPIcs.CSL.2013.563

Quantitative reactive modeling and verification
T.A. Henzinger, Computer Science Research and Development 28 (2013) 331–344.
LibreCat: https://research-explorer.ista.ac.at/record/2289
DOI: 10.1007/s00450-013-0251-7

Computational Methods in Systems Biology
A. Gupta, T.A. Henzinger, eds., Computational Methods in Systems Biology, Springer, 2013.
LibreCat: https://research-explorer.ista.ac.at/record/2288
DOI: 10.1007/978-3-642-40708-6

Local shape analysis for overlaid data structures
C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.
LibreCat: https://research-explorer.ista.ac.at/record/2298
DOI: 10.1007/978-3-642-38856-9_10

Synthesis of AMBA AHB from formal specification: A case study
Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601.
LibreCat: https://research-explorer.ista.ac.at/record/2299
DOI: 10.1007/s10009-011-0207-9

P: Safe asynchronous event-driven programming
A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:, Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, 2013, pp. 321–331.
LibreCat: https://research-explorer.ista.ac.at/record/2301
DOI: 10.1145/2491956.2462184

Aspect-oriented linearizability proofs
T.A. Henzinger, A. Sezgin, V. Vafeiadis, 8052 (2013) 242–256.
LibreCat: https://research-explorer.ista.ac.at/record/2328
DOI: 10.1007/978-3-642-40184-8_18

Automating separation logic using SMT
R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789.
LibreCat: https://research-explorer.ista.ac.at/record/2447
DOI: 10.1007/978-3-642-39799-8_54

Formalizing and reasoning about quality
S. Almagor, U. Boker, O. Kupferman, 7966 (2013) 15–27.
LibreCat: https://research-explorer.ista.ac.at/record/2517
DOI: 10.1007/978-3-642-39212-2_3

Strategy improvement for concurrent reachability and turn based stochastic safety games
K. Chatterjee, L. De Alfaro, T.A. Henzinger, Journal of Computer and System Sciences 79 (2013) 640–657.
LibreCat: https://research-explorer.ista.ac.at/record/2854
DOI: 10.1016/j.jcss.2012.12.001

Mathematical and Engineering Methods in Computer Science
A. Kucera, T.A. Henzinger, J. Nesetril, T. Vojnar, D. Antos, eds., Mathematical and Engineering Methods in Computer Science, Springer, 2013.
LibreCat: https://research-explorer.ista.ac.at/record/2885
DOI: 10.1007/978-3-642-36046-6

How free is your linearizable concurrent data structure?
T.A. Henzinger, A. Sezgin, How Free Is Your Linearizable Concurrent Data Structure?, IST Austria, 2013.
LibreCat: https://research-explorer.ista.ac.at/record/5402
DOI: 10.15479/AT:IST-2013-123-v1-1

Distributed synthesis for LTL fragments
K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25.
LibreCat: https://research-explorer.ista.ac.at/record/1376
DOI: 10.1109/FMCAD.2013.6679386

Distributed synthesis for LTL Fragments
K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.
LibreCat: https://research-explorer.ista.ac.at/record/5406
DOI: 10.15479/AT:IST-2013-130-v1-1

From model checking to model measuring
T.A. Henzinger, J. Otop, 8052 (2013) 273–287.
LibreCat: https://research-explorer.ista.ac.at/record/2327
DOI: 10.1007/978-3-642-40184-8_20

Replacing competition with cooperation to achieve scalable lock-free FIFO queues 
T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013.
LibreCat: https://research-explorer.ista.ac.at/record/6440
DOI: 10.15479/AT:IST-2013-124-v1-1

Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.
LibreCat: https://research-explorer.ista.ac.at/record/5747
DOI: 10.1007/978-3-642-39799-8_11