Deadlock Detection of Java Bytecode
This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language – the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.
We thank Elena Giachino for the fruitful discussions and useful comments, in particular for the help in the proof of Theorem 2.
- 1.Atkey, R., Sannella, D.: ThreadSafe: static analysis for Java concurrency. In: ECEASST, vol. 72 (2015). http://journal.ub.tu-berlin.de/eceasst/article/view/1025
- 3.Eslamimehr, M., Palsberg, J.: Sherlock: scalable deadlock detection for concurrent programs. In Proceedings of the 22nd International Symposium on Foundations of Software Engineering (FSE-22), pp. 353–365. ACM (2014)Google Scholar
- 4.Ferrara, P.: Checkmate: a generic static analyzer of java multithreaded programs. In: Proceedings of 7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, pp. 169–178. IEEE Computer Society (2009)Google Scholar
- 6.Garcia, A.: Static analysis of concurrent programs based on behavioral type systems. Ph.D. thesis, School in Computer Science and Engineering (2017). JaDA.cs.unibo.it
- 11.Laneve, C.: A lightweight deadlock analysis technique of object-oriented programs, January 2018. Submitted for publicationGoogle Scholar
- 12.Laneve, C., Garcia, A.: Deadlock detection of Java Bytecode (full version), November 2017. cs.unibo.it/~laneve/papers/ddJB.pdf
- 13.Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective static deadlock detection. In: 31st International Conference on Software Engineering (ICSE 2009), pp. 386–396. ACM (2009)Google Scholar
- 14.Odersky, M., et al.: An overview of the scala programming language. Technical report IC/2004/64, EPFL, Lausanne, Switzerland (2004)Google Scholar