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.

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

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

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

Local shape analysis for overlaid data structures
C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.

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.

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.

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

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

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

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.

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.

How free is your linearizable concurrent data structure?
T.A. Henzinger, A. Sezgin, How Free Is Your Linearizable Concurrent Data Structure?, IST Austria, 2013.

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.

Distributed synthesis for LTL Fragments
K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.