--- section: 32 x-masysma-name: spark_bmc title: SPARK-BMC Experimental Bounded Model Checker for SPARK (Ada Subset) date: 2025/01/18 16:48:05 lang: en-US author: ["Claudio Belo Lourenco", "Linux-Fan, Ma_Sys.ma (info@masysma.net)"] keywords: ["ada", "spark", "cbmc", "model", "bounded", "experiment", "z"] x-masysma-version: 1.0.0 x-masysma-website: https://masysma.net/32/spark_bmc.xhtml x-masysma-repository: https://www.github.com/m7a/lp-spark-bmc x-masysma-copyright: | Copyright 2013, Claudio Belo Lourenco, Victor Miraldo, Jorge Sousa Pinto Copyright (c) 2025 Ma_Sys.ma . --- 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 * Paper: and * Thesis: ### Original Source Code * `https://bitbucket.org/vhaslab/spark-src` does not contain the change history but a faithful representation of that code may be obtained from here: * Licensed code used as base for creating the current copy: