Introduction

UCLID5 is a software toolkit for the formal modeling, specification, verification, and synthesis of computational systems. The UCLID5 toolchain aims to:

1. Enable compositional (modular) modeling of finite and infinite state transition systems across a range of concurrency models and background logical theories;
2. Verification of a range of properties, including assertions, invariants, and temporal properties, and
3. Integrate modeling and verification with algorithmic and inductive synthesis.

UCLID5 draws inspiration from the earlier UCLID system for modeling and verification of systems {{#cite bryant-cav02}} {{#cite lahiri-cav04}}, in particular the idea of modeling concurrent systems in first-order logic with a range of background theories, and the use of proof scripts within the model. However, the UCLID5 modeling language and verification capabilities go beyond the original modeling language, and the planned integration with synthesis is novel.

This document serves as introduction to the UCLID5 modeling language and toolchain. With the UCLID5 system under active development, we expect this document to undergo several changes as the system and its applications evolve.

Prerequisites

UCLID5 has two prerequisites.

1. UCLID5 requires that the JavaTM Runtime Environment be installed on your machine. You can download the latest Java Runtime Environment for your platform from https://www.java.com.
2. UCLID5 uses the Z3 SMT solver. You can install Z3 from: https://github.com/Z3Prover/z3/releases. Make sure the z3 or z3.exe binary is in your path after Z3 installed. Also make sure, the shared libraries for libz3 and libz3java are in the dynamic library load path (LD_LIBRARY_PATH on Unix-like systems). UCLID5 has been tested with JavaTM SE Runtime Environment version 1.8.0 and Z3 versions 4.5.1 and 4.6.0.

TODO: add optional prerequisites (CVC4, other verif. backends?).

Installation Guide

Public releases of the UCLID5 can be obtained at: https://github.com/uclid-org/uclid/releases.

Quick

For the impatient, the short version of the installation instructions is: download the archive with the latest release, unzip the archive and add the bin/ subdirectory to your PATH. More detailed instructions for installation are as follows.

Detailed Installation

First, down the platform independent package from https://github.com/uclid-org/uclid/releases. Next, follow these instructions which are provided for the bash shell running on a Unix-like platform. Operations for Micosoft Windows, or a different shell should be similar.

• Unzip the archive.

  > unzip uclid-0.9.5.zip

• Add the uclid binary to your path.

  > export PATH=$PATH:$PWD/uclid-0.9.5/bin/

• Check that the uclid works.

  > uclid --help

This should produce output similar to the following.

uclid 0.9.5
Usage: uclid [options] <file> ...

  -m, --main <Module>      Name of the main module.
  -s, --solver <Cmd>       External SMT solver binary.
  -y, --synthesizer <Cmd>  Command line to invoke SyGuS synthesizer.
  -g, --smt-file-generation <value>
                           File prefix to generate smt files for each assertion.
  -X, --exception-stack-trace
                           Print exception stack trace.
  -f, --sygus-format       Generate the standard SyGuS format.
  -e, --enum-to-numeric    Enable conversion from EnumType to NumericType.
  -u, --uf-to-array        Enable conversion from Uninterpreted Functions to Arrays.
  -t, --test-fixedpoint    Test fixed point
  --help                   prints this usage text
  <file> ...               List of files to analyze.

Example

Invoke UCLID5 on a model is easy. Just run the uclid binary and provide a list of files containing the model as a command-line argument. When invoked, UCLID5 will parse each of these files and look for a module named main among them. It will execute the commands in the main module’s control block. The --main command line argument can be used to specify a different name for the main module. Note only the main module's control blocks will be executed, even if the main module instantiates other modules with control blocks. If no main module is found, UCLID5 will exit with an error, as we saw in the previous section when uclid was invoked without arguments.

Example 1.1 is part of the UCLID5 distribution in the examples/tutorial/ subdirectory. You can run UCLID5 on this model as:

> uclid examples/tutorial/ex1.1-fib-model.ucl

This should produce the following output.

Successfully parsed 1 and instantiated 1 module(s).
4 assertions passed.
0 assertions failed.
0 assertions indeterminate.
Finished execution for module: main.

A first look at UCLID5

A simple UCLID5 module that computes the Fibonacci sequence is shown in the example shown below for reference.

module main {
    // Part 1: System description.
    var a, b : integer;
    
    init {
        a = 0;
        b = 1;
    }

    next {
        a’, b’ = b, a + b;
    }

    // Part 2: System specification.
    invariant a_le_b: a <= b;

    // Part 3: Proof script.
    control {
        unroll (3);
        check;
        print_results;
    }
}

We will now walk through each line in this model to understand the basics of UCLID5. The top-level syntactic structure in UCLID5 is a module. All modeling, verification and synthesis code in UCLID5 is contained within modules. In the example, we have defined one module named main.

The module can be conceptually split into three parts: a system description, a specification and proof script. In the example, these three conceptual parts are also kept separate in the code. The following subsections describe each of these sections.

The System Model

This part of a UCLID5 module describes the functionality of the transition system that is being modeled: it tells us what the system does. The first item of interest within the module main are state variables. These are declared using the var keyword.

The module main declares two state variables: a and b. These are both of type integer, which corresponds to mathematical integers. The init block appears next, defining the initial values of the state variables in the module. After the init block is executed, a and b have the values 0 and 1 respectively. The next block appears after this and it defines the transition relation of the module. Primed variables (notation a') refer to the value of the state variables at the end of the current "step". The next block assigns a to the (old) value of b, while b is assigned to the (old) value of a + b.

The System Specification

The specification answers the question: what is the system supposed to do?. In our example, we have a single invariant that comprises that entire specification. It is named a_le_b and as the name suggests, it states that a must be less than or equal to b for every reachable state of the system. Note that the keywords invariant and property are synonyms in UCLID5.

The Proof Script

The third and final part of the UCLID5 module is a set of commands to the UCLID5 verification engine. These tell how UCLID5 should go about proving that the system satisfies its specification.

The proof script is contained within the control block. The commands here execute the system for 3 steps and check whether all of the systems properties (in this case, we only have one invariant: a_le_b) are satisfied for each of these steps. The command unroll executes the system for 3 steps. This execution generates four proof obligations. These proof obligations ask whether the system satisfies the invariant a_le_b in the initial state and in each of the 3 states reached next. The check command checks whether these proof obligations are satisfied and the print results prints out the results of these checks.

UCLID5 Language

• Datatypes
• Variables
• Statements
• init, next, control
• Procedures
• Modules
• Full Language Reference

Datatypes

Datatypes

UCLID5 supports the following base datatypes:

1. integer: mathematical integers

2. boolean: the Boolean type with two values: true and false.

3. Bit-vector types bvW: the family of bit-vector types parameterized by their width (W).

   e.g. bv32

4. Enumeration types using the keyword enum:

   e.g. enum { a, b, c}

These types are mapped down to their SMT equivalents.

UCLID5 also allows definition of higher-order types: arrays, records and uninterpreted functions.

5. Arrays are defined by field_type[index_type] where field_type is the type of data members stored in the array and index_type is the type of the array index.

   e.g. bv32[bv4]

6. Records are defined using the record keyword followed by a list of named members.

   e.g. record { valid : boolean, payload : bv32 }

Named typedefs

Named typedefs of the following form are allowed:

type <typename> = <typedefinition>;

For example, message_t is record-type with a 32-bit payload and a boolean valid flag. And regfile_t is an array type with 4-bit index and 32-bit register elements.

type message_t = record { valid : boolean, payload : bv32 };

type regfile_t = bv32[bv4];

These typedefs can be used when instantiating variables as described below.

Example

The following example from illustrates several type definitions defined in the common module. This module can be imported into multiple other modules.

module common {
  // addresses 8-bit vectors
  type addr_t = bv8;
  type word_t = bv8;
  // 
  type mem_t = [addr_t]word_t;
  // CPU operation.
  type op_t   = enum { op_mov, op_add, op_sub, op_load, op_store };
}

Variable Declarations

Variables

Variables in UCLID5 are instantiated using a var declaration as

	var <variable_name> : <type>;

Constants

Symbolic constants are declared using the const keyword as

	const <const_name> : <type>;

Note though that the value for the constant is not defined here.

Uninterpreted functions

Uninterpreted functions are identified by the keyword function: they have a list of input types and an output type. Uninterpreted functions can be declared function declaration. These functions are typed, mapping a tuple of typed arguments to a return type.

	function <function_name>(<input_type_list>) : <output_type>;

For example, the following uninterpreted function models the mapping of an instrution to an opcode.

	function inst2op(i : word_t) : op_t;

Input and output variables

Variables can be marked with the keywords input and output, expressing the fact that these variables can be connected to/from by other external modules. Note that the var keyword is not used. For example:

input my_input_1 : int
output my_output_2 : bv8

We describe this in greater detail in the Modules page.

Accessing values

The syntax for accessing values from these variables with higher-order types is similar to languages like C/Java. Arrays are 0 indexed and use the [] operator. Fields from records are accessed with ..

	var myarr : [int]bool;
	sixthval = myarr[5];

	var myrec : record { valid : bool, payload : bv32 };
	pyld = myrec.payload;

Index i of array arr is accessed using the syntax arr[i]. Field value in the record result is accessed as result.value.

Example

As an example we show an excerpt of an ALU model illustrating input and output declarations as well as internal variable (normal var) declarations. The excerpt is taken from here.

module main {

  // typedef cmd_t which is an enum
  type cmd_t = enum { add, sub, mov_imm };
  // typedef result_t which is a record
  type result_t = record { valid : boolean, value : bv8 };

  input  valid  : boolean;
  input  cmd    : cmd_t;
  // the ALU takes two 3-bit input values from another module
  input  r1, r2 : bv3;
  input  immed  : bv8;
  output result : result_t;
  var    regs   : [bv3]bv8;
  var    cnt    : bv8; 
  
  // ... remaining module content
}

Statements and Imperative Constructs

UCLID5 allows for the following constructs:

• Assignments
• Defines
• For loops
• If then else
• Case statements

Assignments

Computation in UCLID5 can be either procedural (sequential) or parallel (concurrent). Procedural computation is performed either in the init block or by defining a procedure. Parallel computation occurs in the next block.

Comparing Parallel vs. Sequential Assignments

Sequential assignments are of the form:

// a sequential assignment
variable = expression;

The following sequential assignment

  x = x + 1;
  y = x;

behaves exactly as a typical imperative assignment in usual programming languages. If the values at the beginning of the code snippet were x = 0 and y = 1, post execution, the values will be x = 1 and y = 1.

Parallel assignments must be of the form (the prime denotes parallel assignment):

variable' = expression;

The parallel assignment:

  x' = x + 1;
  y' = x;

behaves as if both the statements executed simultaneously. If the values of the variables were x = 0 and y = 1, then after executing the values will be x = 1, y = 0.

Assignments made in procedures and in the init block are sequential assignment while assignments made in the next block are parallel assignments.

We will discuss the init, next blocks as well as procedures in the coming sections.

Duplicate update check

Since parallel assignments update values simultaneously, UCLID5 checks whether the same variable is being written to twice.

The following sequential snippet is allowed and ends with x having the value 6.

x = 1;
x = x + 2;
x = x + 3;

In contrast, the following sequence of parallel assignments is not allowed and will result in a compiler error.

// Error, will not compile.
x' = 1;
x' = x + 2;
x' = x + 3;

Only a single parallel assignment to a state/output variable is allowed in a code block. Furthermore, since parallel assignments are computed in data-flow order, the order in which they are specified does not matter. This means that the following two snippets of code are equivalent:

next {
    x' = x + 1;
    y' = x' + 1;
}

next {
    y' = x' + 1;
    x' = x + 1;
}

UCLID5 determines that since y' depends on the value of x', x' has to be computed first. This value is then used in the computation of y'. This is regardless of the order in which these assignments appear in the next block. Note also that the assignment to x' uses the value of the variable x at the beginning of the current step of the transition system (i.e., the "old" value of x). In contrast the assignment to y' uses the "new" value of x, which is the value of x at the end of this step of the transition system. It is important to think carefully about which version of a variable (var or var') must be used in a particular assignment.

Defines

UCLID5 also supports the definition of C-like macro expressions which identified by the define keyword as follows.

define <name> (arg list) : <return types> = <expression>

e.g. define double(arg : bv8) : bv8 = (arg + arg);

Such definitions are useful, as in C, to define expressions over arguments that are instantiated in multiple places, or which help make the code more readable.

For Loops

UCLID5 begin a verification language does not allow dynamic range (or unbounded) for loops. The range must be specified by numeric literals as follows:

for (i : bv3) in (0bv3, 7bv3) { regs[i] = 1bv8; }

The loop iterates over the values between 0 and 7 (both-inclusive).

In many cases the values 0bv3 and 7bv3 are parameters of the model or are simply replicated across several locations in the code. Hence, UCLID5 also allows defining these values as macro-definitions. This requires the for statement to be declared with a typed iterator. For example, if the following macro definitions are at the module level,

define begin() : bv3 = 0bv3;
define end() : bv3 = 7bv3;

we may alternatively write the for loop in set init state in the following way:

for (i : bv3) in (begin(), end()) { regs[i] = 1bv8; }

If then else

If-then-else statements follow usual imperative syntax.

  if (condition_expression) {
    // then statements
  } else { 
    // else statements
  }

Case statements

UCLID5 supports case statements in the style of case-switch statements in C++. The following snippet illustrates their use.

    case
      (cmd == add)     : { regs[r1] = r1val + r2val; }
      (cmd == sub)     : { regs[r1] = r1val - r2val; }
      (cmd == mov_imm) : { regs[r1] = immed; }
    esac

case statements are delimited by case and esac and contain within them a list of boolean expressions and associated statement blocks. These expressions are evaluated in the order in which appear, and if any of them evaluate to true, the corresponding block is executed. If none of the case-expressions evaluate to true, nothing is executed. The keyword default can be used as a catch-all case like in C/C++.

init, next, control

init block

The init block initializes the variables used in the UCLID5 module. It consists of sequential assignments.

init {
	x = 1; y = 1;
}

next block

The next block models the transition relation of the module.

next {
	// simple parallel assignments
	x' = 1; y' = 0;

	// use of procedures to handle complex assignments
	call (z') = complex_procedure (x, y);

	// transition submodules
	next (a_submodule);
}

All assignments in the next block must be parallel assignments. However, there are cases when complex sequential logic is required to determine the next value of a variable, which is very tedious to implement solely using parallel updates. This can then implemented by performing procedure calls from the next block with the procedure housing the sequential logic.

As is described in the modules.md section, UCLID5 modules can house other submodules, which have their own transition systems (and next blocks). In such cases simultaneous transition of the submodule instance a_submodule can be achieved by using the next function on a_submodule.

control block

The control block is essentially a verification script containing verification actions that are to be performed on the module.

control {
    unroll (3);
    check;
    print_results;
}

The control block should only be a part of the top-level module also termed as the main module. Typical verification actions, which have been described in the introductory examples are unroll (k) (unroll the transition system for k steps), check (perform verification of properties on the unrolled transition system), etc. The resutlts from the verification can be printed using the print_results command. We will disucss more verification strategies in the section on verification.

Procedures

Procedures take in a list of arguments and return a set of named values. The following snippet extracted from the ALU example illustrates use of procedures.

module main {
	// global variables such as valid
	// ... other stuff

	procedure exec_cmd() returns (r : result_t)
		modifies regs;
	{
		var r1val, r2val : bv8;
		if (valid) {
		  r1val, r2val = regs[r1], regs[r2];
		  case
		    (cmd == add)     : { regs[r1] = r1val + r2val; }
		    (cmd == sub)     : { regs[r1] = r1val - r2val; }
		    (cmd == mov_imm) : { regs[r1] = immed; }
		  esac
		  r.valid, r.value = true, regs[r1];
		} else { r.valid = false; }
	}

	// ... other stuff 
}

Modifies, Requires and Ensures

Procedures have three qualifiers: modifies, requires and ensures. The modifies lists a mandatory set of (global) variables which the procedure modifies, requires is a (optional) set of pre-conditions that the procedure needs to satisfy at the call site and ensures is an (optional) set of properties that the procedure guarantees will hold.

The procedure above modifies the global variable regs, and hence regs must be declared in the modifies list of the procedure. UCLID5 complains if the modifies list is not declared correctly.

requires and ensures statements allow for verification of procedures and are optional.

Extending the example above, the following additional requires and ensures statements would require that valid is always true at entry to the function exec_cmd() and gaurantees that the result at index r1 of regs changes according to the command cmd.

    procedure exec_cmd() returns (r : result_t)
        modifies regs;
        requires valid;
        ensures cmd == add => regs = old(regs)[r1 -> old(regs)[r1] + old(regs)[r1]];
        ensures cmd == sub ==> regs == old(regs)[r1 -> old(regs)[r1] - old(regs)[r2]];
        ensures cmd == mov_imm ==> regs == old(regs)[r1 -> immed];
    {
        var r1val, r2val : bv8;
        if (valid) {
          r1val, r2val = regs[r1], regs[r2];
          case
            (cmd == add)     : { regs[r1] = r1val + r2val; }
            (cmd == sub)     : { regs[r1] = r1val - r2val; }
            (cmd == mov_imm) : { regs[r1] = immed; }
          esac
          r.valid, r.value = true, regs[r1];
        } else { r.valid = false; }
    }

Optionally, one may use the -M argument in UCLID5 to infer the modifies sets which computes the modified variables using the LHS assignments within the procedure and the modifies sets computed for any procedure callswithin the procedure body. Example usage: uclid -M filename.ucl.

Calling Procedures

Procedures are called using the call keyword. The syntax of this is rather unconvential.

	call (variable to store return value(s)) = <procedure_name> (argument list);

For example the above procedure can be called as follows.

	call (result') = exec_cmd();

Note how the return value can even be stored into a primed variable (in the next) block. Procedure calls allow complex sequential computation to be made even in the next block.

Procedure Inlining

A procedure also contains an optional no-inline/inline qualifier which instructions the UCLID5 compiler to either inline the procedure body or use the modifies, requires and ensures statements as a summary of the procedure call.

Without specifying a qualifier or if inline is specified:

    procedure [inline] exec_cmd() returns (r : result_t)

The body of the procedure is beta-reduced using the arguments (if any exist) and inlined at the call site. For the example above, because there are no arguments, call exec_cmd() would simply be replaced with the body of the procedure.

The following is an example of using noinline:

    procedure [noinline] exec_cmd() returns (r : result_t)

In the definition above, the noinline qualifier indicates to the compiler to use the specification defined by the modifies, requires and ensures statements instead of using the body of the procedure. In this case, the variables in the modifies set are havoced (new symbolic constants are created), the requires statements are asserted and the ensures statements are assumed. This effectively replaces the procedure call call exec_cmd() with the following:

havoc regs;
assert valid;
assume cmd == add => regs = old(regs)[r1 -> old(regs)[r1] + old(regs)[r1]];
assume cmd == sub ==> regs == old(regs)[r1 -> old(regs)[r1] - old(regs)[r2]];
assume cmd == mov_imm ==> regs == old(regs)[r1 -> immed];

Instance Procedure Calls

NOTE: This section is experimental; instance procedure calls in the next block is not well documented. If your goal is the separately define module state and procedures, please refer to module concatenation.

So far, all procedure calls have been made within their defining modules. However, sometimes one may wish to call procedures from another instance defined within the module. By declaring the instance name before the name of the procedure as follow:

module A {
    // ... other stuff
    procedure foo() {
        // ... other stuff
    }
}

module main {
    instance a: A();
    
    procedure bar() {
        call a.foo();
    }
}

In this example, two modules A and main are defined. An instance of A is instantiated in module main and the procedure bar within main makes an instance procedure call to a.foo(). This executes the procedure foo as if the variables of instance a and foo were defined within the main module.

Modules

UCLID5 provides the the user the ability to model and verify systems in a compositional manner, through the use of modules. All the previous examples had only a single module, the main module. However, one can define multiple modules and instantiate them, allowing module features to be shared across different models as well as different low level implementations for the same high-level interfaces. We illustrate this capability through an example model for a CPU.

Consider a module common which consists all the type definitions for the datatypes used in the CPU module.

// This module declares types that are used in the rest of the model.
module common {
	// addresses are uninterpreted types.
	type addr_t = bv8;
	type word_t = bv8;
	// memory
	type mem_t = [addr_t]word_t;
	// CPU operation.
	type op_t = enum { op_mov, op_add, op_sub, op_load, op_store };
}

These type definitions can then be conveniently imported into other modules. For example we show the cpu module which loads these type definitions. This is an excerpt of the example available here.

module cpu {
  type addr_t = common.addr_t;
  type mem_t  = common.mem_t;
  type word_t = common.word_t;
  type op_t   = common.op_t;

  // remainder of the cpu module
}

Instantiating Modules

The cpu module can then be instantiated as a part of the another module. We give an example where this is the main module, an excerpt from here.

module main {
  // ...  
  // Create two instances of the CPU module.
  instance cpu_i_1 : cpu(imem : (imem));
  instance cpu_i_2 : cpu(imem : (imem));

  init {
  	// ...
  }

  next {
  	// ...
  	// Invoke CPU 1 and CPU 2.
  	next (cpu_i_1);
  	next (cpu_i_2);
  }
  // ...
}

The main module consists of two instances of the cpu module, called as cpu_i_1 and cpu_i_2. These modules can be stepped using the next function as is done in the next block of the main module.

The overall model must have a single top-level module, which by default is the main module. The name of the top-level module module can be provided using the command-line option -m/--main to UCLID5.

	uclid -m <name of top-level module> <files>

Also, the module files must be specified in the order of the dependencies. For the CPU example, main.ucl depends on cpu.ucl which in turn depends on common.ucl, the UCLID5 tool should be invoked as follows.

	uclid common.ucl cpu.ucl main.ucl

Module Concatenation

Up until now, we have only defined uniquely named modules. However, this is limiting in the following ways:

1. Modules with many definitions result in a large file.
2. Verifying modules with varying definitions is cumbersome because one would need to manually swap out the definition everytime or create multiple copies of module files with the different implementations.

Thus UCLID5 allows module concatentation (a purely syntactic feature) to alleviate these issues by simply concatenating all defined modules with the same name into one module containing all the definitions defined in each module. For example, lets say we have the following files A_x.ucl and A_y.ucl:

// Filename: A_x.ucl
module A {
    var x: integer;
    procedure foo()
        modifies x;
    {
        x = x + 1;
    }
}

// Filename: A_y.ucl
module A {
    var y: integer;
    procedure bar()
        modifies y;
    {
        y = y + 1;
    }
}

Then running uclid A_x.ucl A_y.ucl results in running the concatenated module A:

module A {
    var x: integer;
    var y: integer;

    procedure foo()
        modifies x;
    {
        x = x + 1;
    }

    procedure bar()
        modifies y;
    {
        y = y + 1;
    }
}

Language Reference

TODO

UCLID5 Verification

• Specification
• Bounded Model Checking
• Inductive Proofs
• Verifying Refinement
• Verifying Hyperproperties
• Floyd-Hoare
• SMTO

Specification

Embedded Specifications

Assume, axiom

System Specifications

property, invariant

Linear Temporal Logic (LTL) Specifications

Uclid5 supports the specification of module behavior using linear temporal logic (LTL).

Bounded Model Checking (BMC)

Bounded Model Checking (BMC) is a useful technique for bounded verification and bug finding.

(Note: the unroll command is a now deprecated command which performs bounded model checking for non-LTL properties only. bmc performs bounded model checking for both LTL and non-LTL properties)

The Fibonacci example (introduced in A first look at UCLID5) is reproduced below but now with the bmc command, which has the same semantics as the unroll command.

module main {
    var a, b : integer;
    
    init {
        a = 0; b = 1;
    }

    next {
        a’, b’ = b, a + b;
    }

    // This time the invariant will be checked by BMC 
    // 	instead of an inductiveness check.
    invariant a_le_b: a <= b;

    control {
    	// The bmc command
        bmc (3);
        check;
        print_results;
    }
}

The bmc command unrolls the next block for 3 steps, and generates an SMT query for each step which checks whether the system can violate the property at that step.

Checking Embedded Specifications

To demonstrate checking embedded specifications, we now present a variant of the above Fibonacci example.

module main {
    // System description.
    var a, b : integer;
    const flag : boolean;

    procedure set_init()
        modifies a, b;
    {
        havoc a;
        havoc b;
        // embedded assumptions.
        assume (a <= b);
        assume (a >= 0 && b >= 0);
        assume (flag);
    }

    init {
        call set_init();
    }
    next {
        a', b' = b, a + b;
        if (flag) {
            assert (a' <= b');
        } else {
            assert (false);
        }
    }

    // Proof script.
    control {
        unroll (3);
        check;
        print_results;
    }
}   

We have introduced the constant flag on line 4.

    const flag : boolean;

A constant holds a symbolic value that does not change during computation. The initial value of the constant is assigned non-deterministically and can be controlled using assumptions. A second difference with between this and the first example is on lines 12–14, 23 and 25.

Line 12-14:

        assume (a <= b);
        assume (a >= 0 && b >= 0);
        assume (flag);

Line 23:

            assert (a' <= b');

Line 25:

            assert (false);

Instead of using a module-level assumption declarations as in the first example, we have three embedded assumptions in the set init procedure on lines 12–14, and two embedded assertions in the next block on lines 23 and 25.

A module-level assumption is assumed to hold for the solver at every step of execution, while an embedded assumption is assumed “instantaneously” at the location of the statement. In particular, the assumptions on lines 12–14 tells the solver to assume that \\( a \leq b \\), \\( a \geq 0 \\) and \\( b \leq 0 \\) at the end of the set_init procedure. Notice that we are not assigning specific values to a and b, instead we are asking Uclid5 to consider potential values of a and b such that a ≤ b, a ≥ 0 and b ≥ 0. Similarly the assertions on lines 23 and 25 are evaluated at that specific location in the code. In particular the assertion on line 23 is only checked when flag is true, while the assertion one line 25 is checked when flag is false. Since flag is always true in our model, the assertion on line 25 will never fire. In contrast, note that a module-level assertion would be evaluated after the init block and after each execution of the next block.

Note that we use unroll here again because bmc currently ignores embedded specifications. This will be fixed in a future release.

Checking LTL Specifications

We demonstrate checking LTL Specifications using BMC with a UCLID5 model of an intersection with two traffic lights.

The full UCLID5 model:

module main
{
    type light_t = enum { red, yellow, green };
    var step1, step2 : integer;
    var light1, light2 : light_t;

    init {
        light1, step1 = red,   2;
        light2, step2 = green, 1;
    }

    next {
        call (light1', step1') = next_light(light1, step1);
        call (light2', step2') = next_light(light2, step2);
    }

    procedure next_light(light : light_t, step : integer)
        returns (lightP : light_t, stepP: integer)
    {
        if (step == 0) {
            case
            (light == green) : {
                lightP = yellow;
                stepP = step;
            }
            (light == yellow) : {
                lightP = red;
                stepP = 2;
            }
            (light == red) : {
                lightP = green;
                stepP = 1;
            }
            esac
        } else {
            lightP = light;
            stepP = step - 1;
        }
    }

    property[LTL] always_one_red: G(light1 == red || light2 == red);
    // property[LTL] eventually_green:
    //     G(F(light1 == green)) && G(F(light2 == green));

    control {
        v = bmc(10);
        check;
        print_results;
        v.print_cex(light1, step1, light2, step2);
    }
}

Lines 3–39 define the functionality of the traffic light; this part of the model should be familiar.

    type light_t = enum { red, yellow, green };
    var step1, step2 : integer;
    var light1, light2 : light_t;

    init {
        light1, step1 = red,   2;
        light2, step2 = green, 1;
    }

    next {
        call (light1', step1') = next_light(light1, step1);
        call (light2', step2') = next_light(light2, step2);
    }

    procedure next_light(light : light_t, step : integer)
        returns (lightP : light_t, stepP: integer)
    {
        if (step == 0) {
            case
            (light == green) : {
                lightP = yellow;
                stepP = step;
            }
            (light == yellow) : {
                lightP = red;
                stepP = 2;
            }
            (light == red) : {
                lightP = green;
                stepP = 1;
            }
            esac
        } else {
            lightP = light;
            stepP = step - 1;
        }
    }

The current state of the lights are stored in the variables light1 and light2, and these switch from red to green to yellow and back to red. The variables step1 and step2 can be thought of timers, and ensure that each light stays red for three transitions, green for two transitions and stays yellow for a single transition.

The LTL properties are on lines 41-43.

    property[LTL] always_one_red: G(light1 == red || light2 == red);
    // property[LTL] eventually_green:
    //     G(F(light1 == green)) && G(F(light2 == green));

The property always_one_red specifies a safety property which states that at least one of the two lights must be red in every particular cycle. The notation G(φ) refers to the LTL globally operator, while the notation F(φ) refers to the LTL eventually (future) operator. Other supported operators include next-time: X(φ), (strong-)until: U(φ1, φ2) and weak-until: W(φ1, φ2). always_one_red is a safety property. The property eventually_green is an example of liveness property, and specifies that both lights become green infinitely often. The command for bounded verification of LTL properties is the bmc command. This is invoked on line 46.

        v = bmc(10);

Note that, currently, a UCLID5 model can only have one LTL property at a time. This will be fixed in a future release.

Inductive Proofs

Consider the following UCLID5 module that represents the Fibonacci sequence, and suppose we want to perform unbounded verification for the property \(a \leq b\). To do this, instead of the unroll command, we can use the induction command.

module main {
  var a, b : integer;

  init {
    a = 0; b = 1;
  }
  next {
    a', b' = b, a + b;
  }

  // First inductive invariant
  invariant a_le_b: a <= b;

  control {
    // The induction command.
    induction;
    check;
    print_results;
  }
}

When using the induction command as above, UCLID5 checks

1. that the init block guarantees that the invariants hold and
2. that, assuming the invariants hold for some state, taking a step of the transition from that state as defined in the next block guarantees the invariants will continue to hold.

The induction check for the example above will fail the second check: \(a = -1\) and \(b = 0\) satisfy the specification but taking a step from that state will result in \(a = 0\) and \(b = -1\), which does not satisfy the specification. We can remedy this by adding another invariant to the model.

module main {
  // ... same as above 

  invariant a_le_b: a <= b;
  invariant a_ge_0: a >= 0;
  
  // ... same as above
}

Now with the additional, invariant a_ge_0 the combined invariants are inductive, and the check passes.

k-Induction

In the previous example, we used 1-induction to verify that the Fibonacci sequence is increasing. UCLID5 also supports k-induction, which you can use by providing the induction command with a positive integer argument.

When using k-induction, UCLID5 checks

1. that the first k steps, starting from the init block, all guarantee that the invariants hold and
2. that, assuming the invariants hold for k consecutive states, taking one more step of the transition guarantees the invariants will continue to hold.

To better understand k-induction, consider the following UCLID5 module.

module main {
  var x : integer;
  var y : integer;
  var b : boolean;

  init {
    b = true;
    x = 0;
    assume (y > 0);
  }

  next {
    b' = !b;
    if (b) {
        x' = x + 3;
    } else {
        x' = x - 2;
    }
    y' = y + x;
  }

  invariant x_ge_0: x >= 0;
  invariant y_gt_0: y > 0;

  control {
    v = induction(1);
    check;
    print_results;
  }
}

The 1-induction check for the module above will fail. Fortunately, updating the control block to use 2-induction will make the proof pass.

module main {  
  // ... same as above

  control {
      v = induction(2);
      check;
      print_results;
  }  
}

Verifying Refinement

Refinement and simulation

We say that system \(B\) refines system \(A\) if any step taken by \(B\) can be simulated by a sequence of steps by system \(A\) such that the observed effects are identical. As a toy example, consider the two state machines below. Machine \(A\) implements a one-bit counter and outputs \(\texttt{0}\) and \(\texttt{1}\) when in states \(0\) and \(1\) respectively. Machine \(B\) on the other hand implements a two-bit counter: also outputting \(\texttt{0}\) and \(\texttt{1}\) but now in states \(00\) and \(10\) respectively.

The machine \(A\) on the left is refined by the machine \(B\). This is illustrated with the following executions. Any execution of machine \(B\) cycles through its states generating the outputs \(\texttt{0}\) and \(\texttt{1}\) in the green and pink states respectively. But any such execution can be matched with an execution of \(A\), which also generates the same sequence of outputs (albeit in different states). The state coloring identifies a refinement relation: whatever happens in the green (pink) states in \(B\) also happens in the green (pink) states in \(A\).

We observe that third machine \(C\) also refines \(A\) but in a different way: can you find the refinement relation in this case?

Refinement proofs in UCLID5

We can use the features in UCLID5 to specify and hence verify that one system refines another. Typically such a refinement proof takes the form of a following diagram:

Here we want to prove that the system \(A\) (above) is refined by the system \(B\) (below). This requires us to define a refinement relation between states in the two systems as we saw earlier. The proof itself starts by assuming that two states, one each from \(A\) and \(B\), which satisfy the refinement relation. In our example these are \(a_1\) and \(b_1\) respectively.

Then system \(B\) is transitioned for one step, while \(A\) is transitioned for zero or one steps (also called a stuttering transition). Finally the proof checks that the states that result - \(a_2\) and \(b_2\) in our example - also satisfy the refinement relation. This check sets up an inductive proof that \(A\) simulates \(B\) - or \(B\) refines \(A\) as depicted in the figure below.

An example of refinement checking, the verification of a simple pipelined datapath, is illustrated in detail in the code here. Observe that in this example the spec module describes the system that simulates the one described by the impl module.

Hyperproperties

UCLID5 supports the verification of hyperproperties at both the module level and procedural level.

Verifying Module Hyperproperties

One of the major benefits of using UCLID5 is the native support for creating instances. This allows the user to instantiate multiple instances that produce the traces in a hyperproperty. In this section, we present an intuitive way to verify hyperproperties. In the following sections, we present additional sugar-syntax for proving hyperinvariants of modules.

As an example, consider a transition system \(A\): \[A = (V,I,\delta) = ( \{(a, x) | a \in \mathbb{N}, x \in \mathbb{N} \}, \{(a, 0) | a \in\mathbb{N}\}, \{ ((a, x), (a^\prime, x+a)) | a,a^\prime,x\in\mathbb{N}\})\]

with system input \(a\), state variable \(x\), the set of initial states \(I\) and the transition relation \(\delta\).

A hyperproperty one may wish to prove is that the system is deterministic given that the inputs are the same, which can be specified as: \[ \forall i\in\mathbb{N}. (\pi_1^i.a = \pi_2^i.a) \implies (\pi_1^i.x = \pi_2^i.x) \]

where \(\pi_1, \pi_2\) are traces of the system \(A\) and \(\pi_1^i, \pi_2^i\) are the \(i\)-th states of the trace \(\pi_1, \pi_2\) respectively. We also write \(\pi_1^i.a\) to mean the value of the variable \(a\) at state \(\pi_1^i\) and similarly for other other variable and traces.

To prove such a property, one would first define the transition system \(A\) like this

// Filename: a.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }
}

and then create a main module which consists of the proof of the specification. The proof would consist of instantiating two traces of \(A\), \(\pi_1\) and \(\pi_2\), and specifying the invariant \( \forall i\in\mathbb{N}. \pi_1^i.x = \pi_2^i.x \). Note that the antecedent of the implication above is implicitly assumed when \(a\) is used as an input to both instances (and hence are always equal between the two traces).

// Filename: a_determinism.ucl
module main {
    var a: integer;

    // Two instances of A
    instance pi1: A(a: (a));
    instance pi2: A(a: (a));

    // Hyperproperty
    invariant determinism: pi1.x == pi2.x;

    // Step both instances by executing them synchronously and havoc the input a
    next {
        havoc a;
        next(pi1); next(pi2);
    }

    // Use inductive model checking to prove the hyperproperty over infinite traces
    control {
        v = induction;
        check;
        print_results;
    }
}

Simply run uclid a.ucl a_determinism.ucl to obtain the results.

% uclid a.ucl a_determinism.ucl
Successfully instantiated 2 module(s).
2 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> v: induction_base [Step #0] property determinism @ a_determinism.ucl, line 9
  PASSED -> v: induction_step [Step #1] property determinism @ a_determinism.ucl, line 9
Finished execution for module: main.

Hyperinvariants

Alternatively, one may specify the hyperproperty of the module within the module itself as such:

// Filename: a_hyperinvariant.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }

    hyperinvariant[2] determinism: (a.1 == a.2) ==> (x.1 == x.2);

    control {
        v = bmc(10);
        check;
        print_results;
    }
}

NOTE: UCLID5 only supports hyperinvariant checking for bounded model checking. To verify the module above, run uclid -m A a_hyperinvariant.ucl (this indicates to the solver to run the control block in module A, which defaults to main if not specified).

HyperAxioms

In addition to the hyperinvariant syntax, one can specify a hyperaxiom, which are assumptions over multiple traces at each step. Continuing with our running example, one may rewrite the antecedent of the specification as an axiom:

// Filename: a_hyperaxiom.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }

    hyperaxiom[2]     same_inputs: (a.1 == a.2);
    hyperinvariant[2] determinism: (x.1 == x.2);

    control {
        v = bmc(10);
        check;
        print_results;
    }
}

NOTE: Hyperaxioms are only supported for bounded model checking.

Verifying Procedural Hyperproperties / Modular Product Verification

Up to this point, procedural properties have been specified using modifies, requires and ensures using the module variables and procedure arguments. UCLID5 also supports the verification of hyperproperties of procedural code.

module main {
    procedure isGreaterThanOrEqual(p: integer, q:integer) returns (res: boolean)
    ensures ((res == true) ==> ( p >= q));
    ensures ((res == false) ==> ( p < q));
    ensures ((p.1 == p.2 && q.1 == q.2)  ==> (res.1 == res.2)); //determinism
    {
        res = true;
        if( p < q)
        {
            res = false;
        }
    }

    control {
        v = verify(isGreaterThanOrEqual);
        check;
        print_results;
    }
}

The example above proves that the isGreaterThanOrEqual to indicator function is deterministic based on the inputs specified by line 5:

    ensures ((p.1 == p.2 && q.1 == q.2)  ==> (res.1 == res.2)); //determinism

Similar to the hyperinvariant syntax, the variable of the \(i\)-th trace is referred to using the .i operator, where i is the trace number.

NOTE: As of current, procedural hyperproperties only support the verification of pure functions that do not modify module state.

Floyd-Hoare

SMTO

UCLID5 Synthesis

• Synthesis Basics
• Syntax Guided Synthesis
• SyMO

Synthesis Basics

UCLID5 supports a full integratation of Syntax-Guided Synthesis(SyGuS) across all verification modes. Given any UCLID5 model containing a synthesis function and a verification command and an external SyGuS solver such as CVC5, UCLID5 will generate a SyGuS problem that aims to find a body for the synthesis function such that the UCLID5 model passes verification.

Synthesis Functions

Synthesis functions are identified by the keyword phrase synthesis function: they have a list of input types and an output type, similar to uninterpreted functions. Synthesis functions can be declared function declaration. These functions are typed, mapping a tuple of typed arguments to a return type.

	synthesis function <function_name>(<input_type_list>) : <output_type>;

For example, the following synthesis function models the mapping of an instrution to an opcode.

	synthesis function inst2op(i : word_t) : op_t;

Synthesis functions can be used throughout uclid code in exactly the same way as uninterpreted functions. The SyGuS problem generated by UCLID5 will try to find bodies for all synthesis functions in the UCLID5 model.

Invoking a SyGuS solver

To solve a synthesis problem with UCLID5, UCLID5 should be called with the command line argument -s /path/to/sygus/solver. This will trigger UCLID5 to generate a synthesis problem instead of a verification problem.

Example Synthesis Problem

The following example uses a synthesis function to strengthen the invariant hole, such that the invariant passes verification by induction.

module main {
  // Part 1: System Description .
  var a , b : integer;

  init {
    a , b = 0 , 1;
  }
  next {
    a ' , b ' = b , a + b ;
  }

  // Part 2: System Specification .
  invariant a_le_b : a <= b;

  // Part 3: Synthesis Integration
  synthesis function h (x : integer , y : integer ) : boolean ;
  invariant hole : h(a , b ) ;

  // Part 4: Proof Script .
  control {
    induction ;
    check ;
    print_results ;
  }
}

Syntax Guided Synthesis

SMO

Advanced Features

Idiomatic UCLID5

Tooling

Options

UCLID5 supports multiple command-line options, which include the following.

-m, --main <Module>                 Name of the main module.
-s, --solver <Cmd>                  Command line to invoke external SMT solver binary.
-y, --synthesizer <Cmd>             Command line to invoke SyGuS synthesizer.
-g, --smt-file-generation <value>   File prefix to generate smt files for each assertion.
-X, --exception-stack-trace         Print exception stack trace.
-f, --sygus-format                  (deprecated, enabled by default)
                                    Generate the standard SyGuS format.
-l, --llama-format                  Generates synthesis format for llama.
-e, --enum-to-numeric               Enable conversion from EnumType to NumericType
-M, --mod-set-analysis              Infers modifies set automatically.
-u, --uf-to-array                   Enable conversion from Uninterpreted Functions to Arrays.
-w, --verbosity <value>             Set verbosity level (0-4)

Examples

Specify main module (-m)

Suppose we have a file model.ucl with multiple modules:

module A {
    ...
    property p_a : ...;
    control {
        v = bmc(5);
        check;
        print_results;
    }
}
module B {
    ...
    property p_b : ...;
    control {
        v = verify(...);
        check;
        print_results;
    }
}
module main {
    instance a : A();
    instance b : B();
    ...
    property p_main : ...;
    control {
        v = induction;
        check;
        print_results;
    }
}

UCLID5 requires a top-level module and proves properties declared in that module. By default, UCLID5 looks for a module named main and uses it as the top-level module. In this case, running uclid model.ucl signals UCLID5 to execute the control block in main and prove property p_main. If we want to prove properties in module A or B, we need to specify a top-level module other than main. The -m flag is used for this purpose. For example,

uclid model.ucl -m A

selects A as the top-level module and UCLID5 will attempt to prove property p_a using bmc.

Invoke external SMT solver binary (-s)

UCLID5 supports multiple backend SMT solvers via the SMTLIB2 interface. By default, UCLID5 uses the Z3 solver. To invoke an alternative solver, such as CVC4, we can use the -s option. For example,

uclid <file.ucl> -s cvc4

// ### Invoke SyGuS synthesizer

Generate SMT files for each assertion (-g)

Using the -g flag, UCLID5 can generate.smt files which contain the SMT formulae for each property declared. -g also expects a prefix for the filenames. For example,

uclid <file.ucl> -g "debug"

generates SMT files with filenames with a pattern of debug-xxx.smt in the directory where the command is executed.