Skip to content

HW5 ‐ Software Model Checking

Jump to bottom
Csanád Telbisz edited this page Sep 24, 2024 · 5 revisions

The goal of this homework is to implement a simple model checker using a bounded model checking (BMC) algorithm for control flow automata (CFA).

Overview

To start working with this homework, be familiar with the materials of these lectures some weeks ago:

  • Program semantics
  • Software verification (BMC & CEGAR)

We suggest reading this presentation about BMC tailored to the needs of this homework. It also contains a flowchart of the BMC algorithm with some annotations related to this homework.

You can find a prepared project under hw5-program-verification-1 in the repository. The project depends on some useful core utilities of the Theta model checking framework included as a JAR file in the lib folder. We use the defined CFA formalism of Theta as well as some of its utility functions for interfacing with SMT solvers.

You have to submit the final version of your project as a zip file including only your src folder.

Buiding with Gradle

  • ./gradlew build

Make sure to run the tests with Gradle so that the library path is set correctly. If you get an unsatisfied link error on Windows, try installing/updating the Microsoft Visual C++ Redistributable Packages 2012.

Expect the build to fail at the beginning due to missing implementation and failing tests. To make sure there is no other problem with the build, you can comment the assertions in BoundedModelCheckerTest class. Don't forget to uncomment them after finishing the implementation.

Tasks

Task 1: Define Semantics of Statements

You have to define the semantics of needed statements in the StmtToExprVisitor class. For each statement, you need to return an expression describing the semantics of the statement and the (potentially) updated indexing as a StmtUnfoldResult object.

Hints:

  • First, explore the available properties of the different statements: it might help you find out what you need to do.
  • A VarIndexing object associates indices (versions) to variables. Use the inc method of VarIndexing to increment the version of a variable when assigned (relevant for writing the semantics of assign and havoc statements).
  • ExprUtils.applyPrimes(expr, indexing) replaces each variable in the expression with its corresponding primed version primed as many times as defined by the indexing (e.g., if the index 2 is associated to x in the indexing, then occurrences of x in expr will be replaced by x'') and returns the new expression.
  • AbstractExprs.Eq(expr1, expr2) creates an equality expression between expr1 and expr2.
  • BoolExprs.True() creates an expression representing true.

Task 2: Implement the Bounded Model Checking Algorithm

Implement the BMC algorithm in the check method of the BoundedModelChecker class. You can find some extra hints in the source code.

Passing all tests in BoundedModelCheckerTest is a necessary condition for passing the assignment. Also, avoid using any external libraries in your implementation other than the ones already defined. Do not unwind the CFA in a depth-first manner.

Remember: you only need to modify the code of the BoundedModelChecker and StmtToExprVisitor classes.

Clone this wiki locally