Home › Downloads

Bakar Kiasan

About

Kiasan is a symbolic execution framework. It provides symbolic simulation of models that is better suited for modular reasoning of strong properties of open systems such as for checking software contracts following the Design-by-Contract (DBC) paradigm.
Bakar means “spark or fire” and Kiasan means "to reason with analogy or symbolically" in Indonesian.

Installing the Bakar Kiasan Eclipse Plugin

  • Download and unpack the SPARK 2011, Eclipse 3.7.2, and Yices 1.0.34 bundles that are appropriate for your architecture
  • Download and unpack the Bakar Kiasan Eclipse Plugin
    The plugin contains seven folders. Move each of them into the ‘dropins’ folder of the Eclipse bundle you installed in the previous step.

    If you are upgrading to a newer release then you should first delete all of the sub-directories under Eclipse's 'dropins' folder.

    Releases

    2012.05.07-1414 - download

    • Fix: Kiasan bound violations were not being reported

    2012.05.04-1535 - download

    • Enhancement: Added 'Run sparkmake' button

    2012.05.01-1037 - download

    • Enhancement: 'Save and Launch' dialog presented when unsaved editors exist prior to launching any Bakar or Spark tool
    • Fix: Kiasan's report generator was crashing when analysis did not find any complete paths (e.g. unsatisfiable pre-condition)

    2012.04.23-2224 - download

    • Fix: Backtracking bug

    2012.04.19-2123 - download

    • Enhancement: Added preference group option which sets the directory where HTML reports will be generated
    • Enhancement: Added preference group option which sets where the dot executable can be found (see graphviz.org)
    • Fix: Various path-related fixes to allow HTML report generation under Windows

    2012.04.19-0816 - download

    • Enhancement: 'Save and Launch' dialog presented when dirty editors exist prior to invoking Kiasan
    • Fix: Invalid scalar constraints were being added for certain paths

    2012.04.17-1949 - download

    • Fix: NoSuchElementException was being raised when Kiasan was invoked on an entire package

    2012.04.14-1737 - download

    • Enhancement: Resized T#, E#, and Time columns in Kiasan Report View

    2012.04.14-1629 - download

    • Enhancement: Added preference group option to always run Examiner before running Kiasan (enabled by default)
    • Enhancement: Added button to toolbar which deletes old Kiasan reports
    • Enhancement: Added preference group option to always delete old Kiasan reports before re-running (enabled by default)

    2012.04.12-1651 - download

    • Enhancement: user notified when Spark Examiner indicates program is free of semantic errors

    2012.04.11-2154 - download

    2011.05.12-1605 - download

    • Fix: uninitialized boolean values in preconditions were not handled correctly
    • Enhancement: refined post-state snapshots when Kiasan uncovers errors
    • Enhancement: Kiasan reports no longer shows out parameters of procedures as return values

    2011.05.05-1732 - download

    • Fix: Arrays were always rendered as 0-based in the Cases graph based view
    • Enhancement: Added support for the 'xor' operator within contracts

    2011.05.04-0218 - download

    2011.04.27-1544 - download

  • (OPTIONAL) Place the Yices executable into your system’s environment path

Using the Plugin

Instructional Video
sort.zip

Getting Help

Question or comments regarding the plugin should be sent to belt@ksu.edu. You might also be able to catch Jason in N324 (typically M-F 10am - 5pm)