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.
Sireum is based on previous extensive efforts in the Bogor model checking framework, the Kiasan symbolic execution framework, and the Indus static analysis framework, the Bandera Java model checker at SAnToS Laboratory. In contrast to previous efforts, Sireum aims to provide a parallelizable, software description (e.g., programming language) agnostic implementation of the above frameworks in a unified platform.
The development of Sireum is supported in part by the US Air Force Office of Scientific Research grant no. FA9550-09-0138. It was also supported by the US National Science Foundation (NSF) CAREER award CCF-0644288, Rockwell Collins Advanced Technology Center, and Lockheed Martin Advanced Technology Laboratories. Any opinions, findings, conclusions, or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the previously mentioned institutions.