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

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.

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

Structural Counter Abstraction
K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.

Analysis of dynamic message passing programs
D. Zufferey, Analysis of Dynamic Message Passing Programs, Institute of Science and Technology Austria, 2013.

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

Efficient synthesis for concurrency by semantics-preserving transformations
P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2013, pp. 951–967.

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

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.

Forgiver triumphs in alternating prisoner's dilemma 
B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, PLoS One 8 (2013).

TTP: Tool for tumor progression
J. Reiter, I. Boei, K. Chatterjee, M. Nowak, in:, Proceedings of 25th Int. Conf. on Computer Aided Verification, Springer, 2013, pp. 101–106.

TTP: Tool for Tumor Progression
J. Reiter, I. Bozic, K. Chatterjee, M. Nowak, TTP: Tool for Tumor Progression, IST Austria, 2013.

Forgiver triumphs in alternating prisoner's dilemma 
B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, (2013).

Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
K. Chatterjee, M. Henzinger, M. Joglekar, N. Shah, Formal Methods in System Design 42 (2013) 301–327.

Automated analysis of real-time scheduling using graph games
K. Chatterjee, A. Kößler, U. Schmid, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, ACM, 2013, pp. 163–172.

Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies
S. Tragust, L.V. Ugelvig, M. Chapuisat, J. Heinze, S. Cremer, BMC Evolutionary Biology 13 (2013).

Ants disinfect fungus-exposed brood by oral uptake and spread of their poison
S. Tragust, B. Mitteregger, V. Barone, M. Konrad, L.V. Ugelvig, S. Cremer, Current Biology 23 (2013) 76–82.

Stable length estimates of tube-like shapes
H. Edelsbrunner, F. Pausinger, in:, 17th IAPR International Conference on Discrete Geometry for Computer Imagery, Springer, 2013, pp. XV–XIX.

Persistent homology in image processing
H. Edelsbrunner, in:, Graph-Based Representations in Pattern Recognition, Springer Nature, Berlin, Heidelberg, 2013, pp. 182–183.

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, 2013.