Home¶

Sireum Strawberry stable and dev are now available at Docker Hub.    Amandroid has been released!

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. 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 was supported in part by the US Air Force Office of Scientific Research grant no. FA9550-09-0138, the US National Science Foundation (NSF) CAREER award CCF-0644288, Rockwell Collins Advanced Technology Center, and Lockheed Martin Advanced Technology Laboratories.

Sireum source (private) repositories are kindly provided by GitHub.

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.

SAnToS Laboratory
Computing & Information Sciences Department
Kansas State University
234 Nichols Hall
702 Mid-Campus Drive South
Manhattan, KS 66506
Phone: (785) 532-6350
Fax: (785) 532-7353
Email: contact@santoslab.org