2017/09/13 by Abel Garcia, Garcia, Abel, Cosimo Laneve +1
Computer Science · #Advanced Software Engineering Methodologies #Formal Methods in Verification #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1709.04152
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.