资 源 简 介
Sireum is a long-term research effort to develop an over-arching software analysis platform that incorporates various static analysis techniques such as data-flow framework, model checking, symbolic execution, abstract interpretation, and deductive reasoning techniques (e.g., using weakest precondition calculation). It can be used to build various kinds of software static analyzers for different kinds of properties.
Homepage
Sireum/Kiasan for Java
Sireum/Kiasan for Java is a JML contract-based automatic verification and test case generation tool-set for Java program units. In contrast to regular unit testing methods, Kiasan does not need input parameters for checking units. Without assertions or contracts (e.g., pre-/post-conditions), Kiasan, by default, detects possible uncaught runtime exceptions such as NullPointerException, ArithmeticException, ArrayIndexOutOfBoundsException, etc. W
