Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p.

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

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

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

Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. 2013. Quantitative relaxation of concurrent data structures. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language. POPL: Principles of Programming Languages, 317–328.

Cerny P, Henzinger TA, Radhakrishna A. 2013. Quantitative abstraction refinement. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language. POPL: Principles of Programming Languages, 115–128.

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

Michaliszyn J, Otop J. 2013. Elementary modal logics over transitive structures. 23, 563–577.

Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer Science Research and Development. 28(4), 331–344.

Gupta A, Henzinger TA eds. 2013. Computational Methods in Systems Biology, Springer,p.

Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.

Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 15(5–6), 585–601.

Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. 2013. P: Safe asynchronous event-driven programming. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Programming Languages Design and Implementation, 321–331.

Henzinger TA, Sezgin A, Vafeiadis V. 2013. Aspect-oriented linearizability proofs. 8052, 242–256.

Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT. 8044, 773–789.

Almagor S, Boker U, Kupferman O. 2013. Formalizing and reasoning about quality. 7966(Part 2), 15–27.

Chatterjee K, De Alfaro L, Henzinger TA. 2013. Strategy improvement for concurrent reachability and turn based stochastic safety games. Journal of Computer and System Sciences. 79(5), 640–657.

Kucera A, Henzinger TA, Nesetril J, Vojnar T, Antos D eds. 2013. Mathematical and Engineering Methods in Computer Science, Springer,p.

Henzinger TA, Sezgin A. 2013. How free is your linearizable concurrent data structure?, IST Austria, 16p.

Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25.