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

Cited in 0 Serials

Citations by Year