Java PathFinder swMATH ID: 7658 Software Authors: Havelund, Klaus; Pressburger, Thomas Description: Model checking JAVA programs using JAVA PathFinder. The paper describes a translator called JAVA PATHFINDER (JPF), which translates from JAVA to PROMELA, the modeling language of the SPIN model checker. JPF translates a given JAVA program into a PROMELA model, which then can be model checked using SPIN. The JAVA program may contain assertions, which are translated into similar assertions in the PROMELA model. The PSIN model checker will then look for deadlocks and violations of any stated assertions. JPF generates a PROMELA model with the same state space characteristics as the JAVA program. Hence, the JAVA program must have a finite and tractable state space. The work should be seen in a broader attempt to make formal methods applicable within NASA’s areas such as space, aviation, and robotics. The work is a continuation of an effort to formally analyze, using SPIN, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications. Homepage: http://javapathfinder.sourceforge.net/ Keywords: program verification; Java; model checking; Spin; concurrent programming; assertions; deadlocks Related Software: SPIN; Bandera; veriSoft; CUTE; DART; dSPIN; BLAST; NuSMV; Korat; Bebop; SLAM; Symstra; Bogor; PVS; Pex; CBMC; Uppaal; CESAR; KLEE; JML Cited in: 92 Publications all top 5 Cited by 209 Authors 6 Dwyer, Matthew B. 6 Hatcliff, John 5 Roşu, Grigore 4 Havelund, Klaus 4 Robby, Matthew 4 Sharygina, Natasha 3 Iosif, Radu 3 Visser, Willem 3 Yorav, Karen 2 Ball, Thomas 2 Brucker, Achim D. 2 Chaki, Sagar 2 Clarke, Edmund Melson jun. 2 Degrave, François 2 del Mar Gallardo, María 2 Ganai, Malay K. 2 Godefroid, Patrice 2 Grumberg, Orna 2 Gupta, Aarti 2 Holzer, Andreas 2 Katz, Shmuel 2 Kofroň, Jan 2 Kröning, Daniel 2 Li, Xuandong 2 Merino, Pedro 2 Meseguer Guaita, José 2 Păsăreanu, Corina S. 2 Schrijvers, Tom 2 Sen, Koushik 2 Tautschnig, Michael 2 Vanhoof, Wim 2 Veith, Helmut 2 Wolff, Burkhart 1 Agha, Gul A. 1 Aguirre, Nazareno M. 1 Alur, Rajeev 1 Arroyo, Marcelo 1 Ashar, Pranav 1 Balakrishnan, Gogul 1 Barnat, Jiří 1 Barner, Sharon 1 Barone-Adesi, Katerina 1 Beckert, Bernhard 1 Bernadsky, Mikhail 1 Betin-Can, Aysu 1 Beyer, Dirk 1 Bozga, Marius 1 Braghin, Chiara 1 Brauer, Jörg 1 Browne, James C. 1 Bu, Lei 1 Bultan, Tevfik 1 Bushnell, David H. 1 Calder, Muffy 1 Chen, Feng 1 Chen, Xin 1 Chen, Xinwei 1 Choi, Yunja 1 Christakis, Maria 1 Chugunov, Gennady 1 Cohen, Ernie 1 Cook, Byron 1 Corbett, James C. 1 Corona, Gabriel 1 Courbis, Roméo 1 Cui, Meng 1 de Boer, Frank S. 1 de la Cámara, Pedro 1 Dennis, Louise Abigail 1 D’Souza, Deepak 1 DuVarney, Daniel C. 1 Edelkamp, Stefan 1 Engel, Christian 1 Engstrom, Eric 1 Erzberger, Heinz 1 Farzan, Azadeh 1 Ferenc, Rudolf 1 Garavel, Hubert 1 George, Chris W. 1 Giannakopoulou, Dimitra 1 Glazberg, Ziv 1 Gligorić, Miloš V. 1 Godio, Ariel 1 Goldman, Max 1 Graf, Susanne 1 Groce, Alex 1 Gurov, Dilian 1 Guthmuller, Marion 1 Hähnle, Reiner 1 Héam, Pierre-Cyrille 1 Heere, Karen 1 Hegedűs, Peter 1 Holzmann, Gerard J. 1 Hoosier, Matthew 1 Hu, Yi-Qi 1 Huang, Hai Feng 1 Huch, Frank 1 Huisman, Marieke 1 Ivančić, Franjo 1 Iyer, S. Purushothaman ...and 109 more Authors all top 5 Cited in 17 Serials 10 Formal Aspects of Computing 8 Formal Methods in System Design 2 Theoretical Computer Science 2 Science of Computer Programming 1 Acta Cybernetica 1 Journal of Computer and System Sciences 1 Programming and Computer Software 1 Journal of Automated Reasoning 1 Journal of Logic and Computation 1 Annals of Mathematics and Artificial Intelligence 1 Informatica (Vilnius) 1 Fundamenta Informaticae 1 1 The Journal of Logic and Algebraic Programming 1 Theory and Practice of Logic Programming 1 Computer Science Review 1 Journal of Logical and Algebraic Methods in Programming Cited in 3 Fields 91 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 1 Systems theory; control (93-XX) Citations by Year