SPARK-BMC Experimental Bounded Model Checker for SPARK (Ada Subset)

Abstract

SPARK-BMC (sometimes also referred to as spark-src) is a research tool to run bounded model checking (BMC) on Spark programs where Spark is a subset of the Ada programming language.

This repository provides the most recent copy of the tool SPARK-BMC patched to be compilable in 2025 on a Debian 12 system.

Warning

This code is imported from the original as-is. I don’t know anything about Haskell and have enabled the compilation of the tool purely by means of trial’n’error.

It is expected that the code contains bugs.

Also, as of now, this code is not maintained. One should be grateful that it is at all available as a starting point to apply bounded model checking to an Ada-like programming language.

License

This project is available under a 3-clause BSD license:

Copyright 2013, Claudio Belo Lourenco, Victor Miraldo, Jorge Sousa Pinto

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.

3. Neither the name of the copyright holder nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
“AS IS” AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Build Instructions

Dependencies

Dependency Debian Package
Z3 z3
GHC ghc
Cabal cabal-install

For further dependencies refer to the list in Spark.cabal

Compile

git clone https://www.github.com/m7a/lp-spark-bmc
cabal configure
cabal build

This generates an executable spark-bmc in a deeply nested subdirectory. In my case it could be found under ./dist-newstyle/build/x86_64-linux/ghc-9.0.2/Spark-0.2/x/spark-bmc/build/spark-bmc/spark-bmc

Example Invocation

Call

.../spark-bmc -e Property -u assert -b 11 -s bit-vec Examples/BinarySearch/Main.adb

Expected Output

Simplification
Renaming identifiers to capture context
Inlining subprograms
Removing attributes and enumerations
Loop unwinding
SSA transformation
CNF transformation
Removing exit statements left by loop unwinding
Creating C and P
Creating Z3 expressions
Exporting to Z3...
WARNING: unknown parameter 'model_completion'
Legal parameters are:
  auto_config (bool) (default: true)
  debug_ref_count (bool) (default: false)
  dot_proof_file (string) (default: proof.dot)
  dump_models (bool) (default: false)
  model (bool) (default: true)
  model_validate (bool) (default: false)
  proof (bool) (default: false)
  rlimit (unsigned int) (default: 0)
  smtlib2_compliant (bool) (default: false)
  stats (bool) (default: false)
  timeout (unsigned int) (default: 4294967295)
  trace (bool) (default: false)
  trace_file_name (string) (default: z3.log)
  type_check (bool) (default: true)
  unicode (bool)
  unsat_core (bool) (default: false)
  well_sorted_check (bool) (default: false)

Solving ...


UNSAT - that means the model is correct

See Also

This section collects some links to the original information about this program.

Academic Paper and Thesis

Original Source Code


Ma_Sys.ma Website 5 (1.0.2) – no Flash, no JavaScript, no Webfont, no Copy Protection, no Mobile First. No bullshit. No GUI needed. Works with any browser.

Created: 2025/01/18 16:48:05 | Tags: ada, spark, cbmc, model, bounded, experiment, z | Version: 1.0.0 | SRC (Pandoc MD) | GPL

Copyright 2013, Claudio Belo Lourenco, Victor Miraldo, Jorge Sousa Pinto Copyright (c) 2025 Ma_Sys.ma info@masysma.net.