Assume-guarantee synthesis for digital contract signing
K. Chatterjee, V. Raman, Formal Aspects of Computing 26 (2013) 825–859.

Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems
K. Chatterjee, V. Prabhu, Information and Computation 228–229 (2013) 83–119.

Trading performance for stability in Markov decision processes
T. Brázdil, K. Chatterjee, V. Forejt, A. Kudera, in:, 28th Annual ACM/IEEE Symposium, IEEE, 2013, pp. 331–340.

What is decidable about partially observable Markov decision processes with omega-regular objectives
K. Chatterjee, M. Chmelik, M. Tracol, 23 (2013) 165–180.

What is decidable about partially observable Markov decision processes with <9-regular objectives
K. Chatterjee, M. Chmelik, M. Tracol, What Is Decidable about Partially Observable Markov Decision Processes with <9-Regular Objectives, IST Austria, 2013.

The complexity of ergodic games
K. Chatterjee, R. Ibsen-Jensen, The Complexity of Ergodic Games, IST Austria, 2013.

Perfect-information stochastic mean-payoff parity games
K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, Perfect-Information Stochastic Mean-Payoff Parity Games, IST Austria, 2013.

The complexity of partial-observation stochastic parity games with finite-memory strategies
K. Chatterjee, L. Doyen, S. Nain, M. Vardi, The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies, IST Austria, 2013.

Density games
S. Novak, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 334 (2013) 26–34.

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

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.

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

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.

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

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.