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 Indus static analysis framework, the Bogor model checking framework, the Kiasan symbolic execution framework, and the Bandera Java model checker at SAnToS Laboratory, Kansas State University. 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. Sireum will initially consist of the following nine components: Base, Pilar, Tipe, Alir, BogorII, KiasanII, Kondisi, Niskala, and Topi.

While Sireum is first and foremost developed as a research vehicle for experimenting with formal methods, it is also designed for teaching various courses such as compiler, program analysis, logical reasoning, and model checking. Extensive pedagogical materials such as lecture notes and slides will be developed to accompany the software infrastructure.

The development of Sireum is supported in part by the US National Science Foundation (NSF) CAREER award CCF-0644288, the US Air Force Office of Scientific Research, and Rockwell Collins Advanced Technology Center. It was also supported by Lockheed Martin Advanced Technology Laboratories.

Sireum means "ants" in the real Java language, i.e., Javanese.