SmpSL Verification Conditions Generator

The tool SmpSL Verification Conditions Generator receives as input a SmpSL program with its specification and computes the verification condition.

The language SmpSL

SmpSL is a simple script language with the embedded SQL commands SELECT, INSERT, UPDATE, and DELETE based on arXiv:1610.02101. See Section 3 of arXiv:1610.02101 for the definition of the language.

The specification logic FO2BD

FO2BD is the two-variable fragment extended with bounded domains. Bounded domains are fixed finite sets. FO2BD extends FO2 by allowing quantification on an unbounded number of variables, under the restriction that all variables aside from two range over the bounded domains only. Two variables may range over the unbounded domain. A FO2BD formula which does not quantify over the bounded domains is a FO2 formula. FO2BD imposes the restriction on the vocabulary that every relation has at most two columns ranging over the unbounded domain.

For example, assume we have one bounded domain: b = {true, false}. The following sentence says that the first two columns of T form the key of T.

(∀d x ∀d y ∀b s1b s2 ((s1 = s2) ∨ ~T(x,y,s1) ∨ ~T(x,y,s2)

The quantifier ∀d ranges over the unbounded domain. The quantifier ∀b ranges over b.

For a more detailed explanation of FO2BD and more examples see Sections 3.3.3 and Section 2 of arXiv:1610.02101

Input of SmpSL VC generator

The input file to our tool consists of four sections:

• The list of tables
• a precondition following the keyword requires,
• the program, and
• a postcondition following the keyword ensures.

List of tables

It is a list of expressions of the form:

• (TableName i)
• (TableName i BOUNDED r1 r2 …)

i is either 1 or 2. i indicates the number of columns ranging over the unbounded domain. After the keyword BOUNDED are the sizes of the bounded domains for any additional column.

For instance, (Users 1) (Subscriptions 2) indicates that the database has two tables, one table with a single column (column1) and the other with two columns (column1 and column2), all of which range over the unbounded domains. Another example: (Papers 2 BOUNDED 3 4) (Authors 2) (Conflicts 2) indicates there are three tables. Papers has four columns, column1 and column2 ranging over the unbounded domain, and b0 and b1 ranging over domains of sizes 3 and 4 respectively.

Precondition

The precondition is of the form:
requires F
where F is an FO2BD sentence.

For instance:

```requires exists nl (~(nl = newsletter) & forall y (Users(y) -> Subscriptions(nl, y)))
```

Note that we do not indicate whether variables range over bounded or unbounded domains neither in the name of the variable nor in the quantifier. A variable may take any name (including but not limited to x and y), and its type (unbounded/bounded domain) is determined by its usage according to the types of the columns.

Another example:

```(Papers 2 BOUNDED 3 5) (Authors 2) (Conflicts 2) (ReviewerBids 2)  (Reviewers 2 BOUNDED 2)  (ReviewerAssignments  2) (Out 1 BOUNDED 5)

requires forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &
forall x y (Out(x,y) <-> exists z w (Papers(x, z, w, y) & Authors(currentUser, x)))
```

Program

The program consists of SELECT, INSERT, UPDATE, DELETE and if commands. Some examples of programs:

`INSERT INTO Subscriptions VALUES (newsletter,user) ; `
```if (IsNotEmpty(SELECT G.Column1 FROM G WHERE Column1 = bidId))
INSERT INTO ReviewerBids VALUES (currentUser, bidId);
else
skip ;
```
`UPDATE Out SET b0 = 0:5 WHERE b0 = 2:5 OR b0 = 3:5 OR b0 = 4:5;`

Postcondition

The postcondition is of the form:
requires F
where F is an FO2BD sentence. F has the same format as in the precondition.

Examples of input files

```(Users 1) (Subscriptions 2)

requires
exists x (~(x = newsletter) & forall y (Users(y) -> Subscriptions(x, y)))

INSERT INTO Subscriptions VALUES (newsletter,user) ;

ensures
forall u (Users(u) -> exists x (Subscriptions(x, u)))
```
```(Papers 2 BOUNDED 3 3) (Authors 2) (Conflicts 2) (ReviewerBids 2)  (Reviewers 2 BOUNDED 2)  (ReviewerAssignments  2)

requires
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &&
ReviewerBids(reviewer, assignId)

INSERT INTO ReviewerAssignments VALUES (reviewer, assignId) ;

ensures
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y))
```
```(Papers 2 BOUNDED 3 5) (Authors 2) (Conflicts 2) (ReviewerBids 2)  (Reviewers 2 BOUNDED 2)  (ReviewerAssignments  2) (Out 1 BOUNDED 5)

requires
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &&
forall x y (Out(x,y) <-> exists z w (Papers(x, z, w, y) & Authors(currentUser, x)))

UPDATE Out SET b0 = 0:5 WHERE b0 = 2:5 OR b0 = 3:5 OR b0 = 4:5;

ensures
forall x y (ReviewerBids(x,y) -> ~ Conflicts(x,y)) &&
forall x y (ReviewerAssignments(x,y) -> ~ Conflicts(x,y)) &&
forall title session (Out(title,session) -> (session = 0:5 || session = 1:5))
```

For more examples, see the benchmarks page.

The source code in Java can be downloaded from here:

Output

The tool outputs an smt2 file containing an FO2 sentence compatible with FO2-solver and other solvers that receive smt2 format as input such as Z3 theorem prover. It is guaranteed that the only variables used in the output file are x and y.

An example of an output of the VC generator:

```(declare-sort V 0)
(declare-datatypes () ((B\$2 _0@2 _1@2) (B\$3 _0@3 _1@3 _2@3)))
(declare-fun ReviewerBids (V V) Bool)
(declare-fun ReviewerAssignments (V V) Bool)
(declare-fun Authors (V V) Bool)
(declare-fun Papers (V V B\$3 B\$3) Bool)
(declare-fun Reviewers (V V B\$2) Bool)
(declare-fun Conflicts (V V) Bool)
(declare-fun ReviewerBids_ (V V) Bool)
(declare-fun ReviewerAssignments_ (V V) Bool)
(declare-fun Authors_ (V V) Bool)
(declare-fun Papers_0_0 (V V) Bool)
(declare-fun Papers_0_1 (V V) Bool)
(declare-fun Papers_0_2 (V V) Bool)
(declare-fun Papers_1_0 (V V) Bool)
(declare-fun Papers_1_1 (V V) Bool)
(declare-fun Papers_1_2 (V V) Bool)
(declare-fun Papers_2_0 (V V) Bool)
(declare-fun Papers_2_1 (V V) Bool)
(declare-fun Papers_2_2 (V V) Bool)
(declare-fun Reviewers_0 (V V) Bool)
(declare-fun Reviewers_1 (V V) Bool)
(declare-fun Conflicts_ (V V) Bool)
(declare-const reviewer V)
(declare-const assignId V)
(assert (not (=> (and (and (forall ((x V)) (forall ((y V)) (=> (ReviewerBids x y) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (ReviewerAssignments x y) (not (Conflicts x y)))))) (ReviewerBids reviewer assignId)) (and (forall ((x V)) (forall ((y V)) (=> (ReviewerBids x y) (not (Conflicts x y))))) (forall ((x V)) (forall ((y V)) (=> (or (ReviewerAssignments x y) (and (= x reviewer) (= y assignId))) (not (Conflicts x y)))))))) )
(check-sat)
(get-model)
```

For more examples, see the benchmarks page.

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

FORSYTE organizes CAV 2018

The FORSYTE group is co-organizing the 30th International Conference on Computer Aided Verification (CAV)

FMSD Special Issue in Memoriam Helmut Veith

In memory of Helmut Veith, the founder of the FORSYTE research group, the current issue of the Journal on Formal Methods in System Design is a Special Issue in Memoriam Helmut Veith.