We are currently developing Sireum v2. Sireum Amandroid is the first publicly available major toolset developed on top of Sireum v2.

Below are some projects done in Sireum v1.

Sireum Bakar

Bakar is a toolset for analyzing Spark Ada programs (Bakar means “spark” in Indonesian).

Sireum Bakar currently includes:

  • Alir: an information flow analysis tool for reasoning about Spark’s derive clauses/information flow (Alir means “flow” in Indonesian). Alir visualizes information flows to ease engineers in understanding information dependencies crucial for specifying and verifying Spark’s derive clauses.

    See: SCAM12.

  • Kiasan: a fully automated tool for verifying functional behaviors of Spark programs specified as software contract (Kiasan means “symbolic” in Indonesian). Kiasan is an explicating symbolic execution tool that provides various helpful feedback including generation of counter example for contract refutation, test cases for an evidence of contract satisfaction, verification reports, visual graphs illustrating pre/post states of Spark procedures/functions, etc.

    See: ICSE13, NFM12, HILT12, NFM11, and SIGADA11.

You can install Bakar v1 by following the instruction in Sireum Distro‘s feature Sireum Bakar.

Demo Videos:

We are actively developing Bakar v2 that will have the above tools along with a Spark 2014/Ada 2012 front-end for Java, Scala, and Coq/OCaml.

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.

See: ASE12, SEFM07, TAICPART07, ISoLA06, and ASE06.