W. Ahrendt, B. Beckert, D. Bruns, R. Bubel, C. Gladisch et al., The KeY Platform for Verification and Analysis of Java Programs, Verified Software: Theories , Tools and Experiments -6th International Conference, pp.55-71, 2014.
DOI : 10.1007/978-3-319-12154-3_4

E. Albert, P. Arenas, J. Correas, S. Genaim, M. Gómez-zamalloa et al., Object-sensitive cost analysis for concurrent objects, Software Testing, Verification and Reliability, vol.11, issue.S2, pp.218-271, 2015.
DOI : 10.1145/2331147.2331165

E. Albert, P. Arenas, S. Genaim, and G. Puebla, Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis, Proceedings SAS 2008, pp.221-237, 2008.
DOI : 10.1007/978-3-540-69166-2_15

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, Cost Analysis of Java Bytecode, Programming Languages and Systems, 16th European Symposium on Programming Held as Part of the Joint European Conferences on Theory and Practics of Software Proceedings, pp.157-172, 2007.
DOI : 10.1007/978-3-540-71316-6_12
URL : http://costa.ls.fi.upm.es/%7Edamiano/pubs/esop07.pdf

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode, Formal Methods for Components and Objects, 6th International Symposium, pp.113-132, 2007.
DOI : 10.1007/978-3-540-74061-2_11

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012.
DOI : 10.1016/j.tcs.2011.07.009
URL : https://doi.org/10.1016/j.tcs.2011.07.009

E. Albert, J. Correas, and G. Román-díez, Peak Cost Analysis of Distributed Systems, Proceedings of SAS 2014, pp.18-33, 2014.
DOI : 10.1007/978-3-319-10936-7_2

E. Albert, J. Correas, and G. Román-díez, Non-cumulative Resource Analysis, Proceedings of TACAS 2015, pp.85-100, 2015.
DOI : 10.1007/978-3-662-46681-0_6

E. Albert, S. Genaim, and M. Gómez-zamalloa, Parametric inference of memory requirements for garbage collected languages, Proceedings of the 2010 international symposium on Memory management, ISMM '10, pp.121-130, 2010.
DOI : 10.1145/1806651.1806671

D. E. , A. , and S. Genaim, On the limits of the classical approach to cost analysis, Proceedings of SAS 2012, pp.405-421, 2012.

D. Ancona, V. Bono, M. Bravetti, J. Campos, G. Castagna et al., Behavioral Types in Programming Languages, Foundations and Trends?? in Programming Languages, vol.3, issue.2-3, pp.95-230, 2016.
DOI : 10.1561/2500000031
URL : https://hal.archives-ouvertes.fr/hal-01348054

C. Artho and A. Biere, Applying static analysis to large-scale, multi-threaded Java programs, Proceedings 2001 Australian Software Engineering Conference, pp.68-75, 2001.
DOI : 10.1109/ASWEC.2001.948499
URL : http://www.inf.ethz.ch/~artho/papers/ArthoBiere-ASWEC2001.pdf

R. Atkey, Amortised Resource Analysis with Separation Logic, 2010.
DOI : 10.1007/978-3-642-11957-6_6

R. Atkey and D. Sannella, Threadsafe: Static analysis for java concurrency, ECEASST, p.72, 2015.

R. Atkey and D. Sannella, Threadsafe: Static analysis for java concurrency, ECEASST, p.72, 2015.

R. Barik, Efficient Computation of May-Happen-in-Parallel Information for Concurrent Java Programs, Proceedings of LCPC 2005, pp.152-169
DOI : 10.1007/978-3-540-69330-7_11

S. Bensalem and K. Havelund, Dynamic Deadlock Analysis of Multi-threaded Programs, Hardware and Software Verification and Testing, pp.208-223, 2005.
DOI : 10.1007/11678779_15
URL : http://www.havelund.com/Publications/padtad05.pdf

L. Berman, The complexity of logical theories, Theoretical Computer Science, vol.11, issue.1, pp.71-77, 1980.
DOI : 10.1016/0304-3975(80)90037-7

C. Boyapati, R. Lee, and M. C. Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of OOPSLA 2002, pp.211-230, 2002.
DOI : 10.1145/582419.582440

M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl, Alternating Runtime and Size Complexity Analysis of Integer Programs, Proceedings of TACAS 2014, pp.140-155, 2014.
DOI : 10.1007/978-3-642-54862-8_10

E. Bruneton, Asm 4.0 a java bytecode engineering library, pp.2016-2028

Q. Carbonneaux, J. Ho?mann, and Z. Shao, Compositional certified resource bounds, Proceedings of the 36th PLDI Conference, pp.467-478, 2015.
DOI : 10.1145/2813885.2737955

H. H. Wei-ngan-chin, S. Nguyen, M. Qin, and . Rinard, Memory Usage Verification for OO Programs, Proceedings of SAS 2005, pp.70-86, 2005.
DOI : 10.1007/11547662_7

B. Haskell, R. Curry, W. Feys, and . Craig, Combinatory logic. I, 1958. North-Holland

A. Mohamed, . El-zawawy, A. Hamada, and . Nayel, Type systems based data race detector, Computer and Information Science, vol.5, issue.4, p.53, 2012.

M. Eslamimehr and J. Palsberg, Sherlock: scalable deadlock detection for concurrent programs, Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pp.353-365, 2014.
DOI : 10.1145/1321631.1321746

A. Flores-montoya, E. Albert, and S. Genaim, Mayhappen-in-parallel based deadlock analysis for concurrent objects, Formal Techniques for Distributed Systems -Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques. Proceedings, pp.273-288, 2013.

A. Flores, M. , and R. Hähnle, Resource Analysis of Complex Programs with Cost Equations, Proceedings of 12th Asian Symposium on Programming Languages and Systems, pp.275-295, 2014.
DOI : 10.1007/978-3-319-12736-1_15

N. Stephen, J. C. Freund, and . Mitchell, A type system for the java bytecode language and verifier, J. Autom. Reasoning, vol.30, pp.3-4271, 2003.

A. Garcia and C. Laneve, Static analyzer of resource usage upper bounds, 2015.

E. Giachino, C. Stijn-de-gouw, B. Laneve, and . Nobakht, Statically and dynamically verifiable sla metrics, 2016
DOI : 10.1007/978-3-319-30734-3_15

E. Giachino, E. Broch-johnsen, C. Laneve, I. Ka, and . Pun, Time complexity of concurrent programs --A technique based on behavioural types, Formal Aspects of Component Software -12th International Conference, pp.199-216, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01229068

E. Giachino, N. Kobayashi, and C. Laneve, Deadlock Analysis of Unbounded Process Networks, Proceedings of 25th International Conference on Concurrency Theory CONCUR 2014, pp.63-77, 2014.
DOI : 10.1007/978-3-662-44584-6_6
URL : https://hal.archives-ouvertes.fr/hal-01091749

E. Giachino, C. Laneve, and M. Lienhardt, A framework for deadlock detection in ABS. Software and Systems Modeling, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01229046

J. Gosling, W. N. Joy, and G. L. Steele-jr, The Java Language Specification, 1996.

S. Gulwani, K. Krishna, T. Mehra, and . Chilimbi, SPEED, ACM SIGPLAN Notices, vol.44, issue.1, pp.127-139, 2009.
DOI : 10.1145/1594834.1480898

A. Gurfinkel and S. Chaki, Combining predicate and numeric abstraction for software model checking, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.409-427, 2010.
DOI : 10.1007/s10009-010-0162-x

M. Hentschel, R. Bubel, and R. Hähnle, Symbolic Execution Debugger (SED), Runtime Verification -5th International Conference, RV 2014 Proceedings, pp.255-262, 2014.
DOI : 10.1007/978-3-319-11164-3_21

J. Ho?mann, K. Aehlig, and M. Hofmann, Multivariate amortized resource analysis, Proceedings of POPL 2011, pp.357-370, 2011.

J. Ho?mann, K. Aehlig, and M. Hofmann, Multivariate amortized resource analysis, ACM Trans. Program. Lang. Syst, vol.34, issue.3, p.14, 2012.

J. Ho?mann and Z. Shao, Automatic static cost analysis for parallel programs, 2015. [Online; accessed 11, 2015.

M. Hofmann and S. Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of POPL 2003, pp.185-197, 2003.

M. Hofmann and S. Jost, Type-Based Amortised Heap-Space Analysis, Proceedings of ESOP 2006, pp.22-37, 2006.
DOI : 10.1007/3-540-45332-6_7
URL : http://www.cs.st-andrews.ac.uk/~jost/research/hofmann_jost_esop06_postfinal.pdf

M. Hofmann and D. Rodriguez, Efficient Type-Checking for Amortised Heap-Space Analysis, Proceedings of CSL 2009, pp.317-331, 2009.
DOI : 10.1137/0606031
URL : http://raja.tcs.ifi.lmu.de/download/files/csl09HofRod.pdf

R. Einar-broch-johnsen, R. Hähnle-schäfer, M. Schlatte, and . Ste?en, ABS: A Core Language for Abstract Behavioral Specification, Proceedings of FMCO 2010, pp.142-164, 2011.
DOI : 10.2498/cit.2002.01.01

P. Joshi, M. Naik, K. Sen, and D. Gay, An e?ective dynamic analysis for detecting generalized deadlocks, Proceedings of the 18th International Symposium on Foundations of Software Engineering, pp.327-336, 2010.
DOI : 10.1145/1882291.1882339
URL : http://www.cs.berkeley.edu/%7Epallavi/papers/FSE10.pdf

N. Kobayashi and C. Laneve, Deadlock analysis of unbounded process networks. Available at the journal website
URL : https://hal.archives-ouvertes.fr/hal-01091749

C. Laneve, A type system for JVM threads, Theoretical Computer Science, vol.290, issue.1, pp.741-778, 2003.
DOI : 10.1016/S0304-3975(02)00330-4
URL : https://doi.org/10.1016/s0304-3975(02)00330-4

S. Mathew, Overview of amazon web services. at d0.awsstatic.com/whitepapers/aws-overview.pdf, 2014.

M. Naik, C. Park, K. Sen, and D. Gay, E?ective static deadlock detection, 31st International Conference on Software Engineering, pp.386-396, 2009.
DOI : 10.1109/icse.2009.5070538
URL : http://berkeley.intel-research.net/dgay/pubs/09-icse-deadlock.pdf

J. Navas, M. Méndez-lojo, V. Manuel, and . Hermenegildo, Customizable resource usage analysis for java bytecode, 2008.
DOI : 10.1016/j.entcs.2009.11.015
URL : https://doi.org/10.1016/j.entcs.2009.11.015

M. Odersky, An Overview of the Scala Programming Language, 2004.

P. Permandla, M. Roberson, and C. Boyapati, A type system for preventing data races and deadlocks in the Java Virtual Machine Language: 1, Proceedings of the 2007 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES'07), p.10, 2007.

R. Stata and M. Abadi, A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems, vol.21, issue.1, pp.90-137, 1999.
DOI : 10.1145/314602.314606

. Robert-endre-tarjan, Amortized Computational Complexity, SIAM Journal on Algebraic Discrete Methods, vol.6, issue.2, pp.306-318, 1985.
DOI : 10.1137/0606031

A. Mathison and T. , On computable numbers, with an application to the entscheidungsproblem, J. of Math, vol.58, pp.345-3635, 1936.

B. Wegbreit, Mechanical program analysis, Communications of the ACM, vol.18, issue.9, pp.528-539, 1975.
DOI : 10.1145/361002.361016

A. Williams, W. Thies, and M. D. Ernst, Static Deadlock Detection for Java Libraries, 19th European Conference on Object- Oriented Programming (ECOOP 2005), pp.602-629, 2005.
DOI : 10.1007/11531142_26