JayHorn swMATH ID: 25903 Software Authors: Temesghen Kahsai; Rody Kersten; Philipp Rümmer; Huascar Sanchez; Martin Schäf Description: JayHorn is a software model checking tool for Java. JayHorn tries to find a proof that certain bad states in a Java program are never reachable. These bad states are specified by adding runtime assertions (where some assertions may be generated, e.g., that an object reference must not be Null before being accessed). JayHorn tries to err on the side of precision that is, when it is not able to proof that an assertion always holds, it will claim that the assertion may be violated (this is called soundness). JayHorn is currently sound (modulo bugs) for Java that use a single thread, have no dynamic class loading, and do not perform complex operations in static initializers. Homepage: http://jayhorn.github.io/jayhorn/ Source Code: https://github.com/jayhorn/jayhorn Keywords: R; R package; arXiv_publication Related Software: SeaHorn; z3; FunArray; JPF-SE; JBMC; Spacer; MoCHi; CoVaC; HMC; LOGEN; Ciao; RAHFT; CiaoPP Cited in: 3 Publications all top 5 Cited by 12 Authors 1 Braine, Julien 1 Gallagher, John P. 1 Gonnord, Laure 1 Hermenegildo, Manuel V. 1 Kafle, Bishoksan 1 Klemen, Maximiliano 1 Koskinen, Eric 1 López-García, Pedro 1 Monniaux, David P. 1 Morales, Jose Francisco 1 Terauchi, Tachio 1 Unno, Hiroshi Cited in 0 Serials Cited in 1 Field 3 Computer science (68-XX) Citations by Year