# Experiments

## Source Code used for Queries Q1-Q24 in ASE’10 Publication

#### list2.c:

int partition(int a[], int left, int right) {
int v = a[right], i = left - 1, j = right, t;
for (;;) {
while (a[++i] < v) ;
while (j > left && a[--j] > v) ;
if (i >= j) break;
t = a[i]; a[i] = a[j]; a[j] = t;
}
t = a[i]; a[i] = a[right]; a[right] = t;
return i;
}

int main(int argc, char * argv[]) {
int A[3];
partition(A, 0, 2);
}

#### sort1.c:

#include <stdio.h>
int compare(int a, int b) {
if (a <= b) return 1;
return 0;
}

int unfinished();

void sort(int * a, int len) {
int i, t;
for (i=1; i<len; ++i) {
if (compare(a[i-1], a[i])) continue;
unfinished();
t=a[i]; a[i]=a[i-1]; a[i-1]=t;
}
return;
}

void eval(int * a, int len) {
int i;
for (i=0; i < 3; ++i)
printf("a[%d]=%d\n", i, a[i]);
return;
}

int main(int argc, char * argv[]) {
int i; int A[3];
int verify;
for (i=0; i < 3; ++i)
sort(A, 3);
if (verify) {
assert(compare(A[0],A[1]));
assert(compare(A[1],A[2]));
}
eval(A, 3);
return 0;
}

#### sort2.c:

#include <stdio.h>
int rand_init;
void insert(int * a, int pos) {
int rand;
a[pos] = rand%rand_init;
return;
}
void eval(int * a, int first, int last) {
if (first > last) return;
printf("a[%d]=%d\n", first, a[first]);
eval(a+1, first+1, last);
return;
}
int precond() {
return (rand_init == 7);
}
int postcond() {
return (rand_init == 7);
}
int main(int argc, char * argv[]) {
int i;
int A[3];
int max;

if(max > 0)
init: rand_init = 7;

for (i=0; i<max; ++i)
insert(A, i);

eval(A, 0, max);

return 0;
}

## Experiments Performed for our VMCAI’09 Publication

Source code used in the following experiments:

Source LLOC* Description
kbfiltr.i 4879 Preprocessed device drivers used in [1] for generating test cases
with BLAST.
floppy.i 6435
cdaudio.i 8022
parport.i 20698
parclass.i 45283
matlab.c 2033 An engine controller provided by an industrial collaborator from
the automotive industries. It is generated from a MATLAB/Simulink
model.
statemate.c 637 Taken from the Mälardalen WCET Benchmark [2]: statemate.c was
automatically generated by STARC (STAtechart Realtime Code
generator), nsichneu.c simulates a Petri net, and adpcm.c
implements functionality for adaptive pulse code modulation. In
the benchmark, values of external variables are fixed. We replaced
constant values by nondeterministic input.
nsichneu.c 1471
autopilot.i 3141 Preprocessed sources generated from source code in Papa-Bench [3].
We performed unit tests on periodic tasks of autopilot.i and
fly_by_wire.i. In autopilot.i we replaced the implemented sinus
function by a stub that returns a nondeterministic value because
the implementation of sinus contains an unbounded loop.
fly_by_wire.i 488

*: Logical lines of code, i.e., the number of occurrences of ‘;’.

[1] Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Generating Tests from Counterexamples. In Proceedings of the 26th IEEE International Conference on Software Engineering (ICSE 2004, Edinburgh, May 26-28), pages 326-335, 2004. IEEE Computer Society Press, Los Alamitos (CA).

Experimental results for basic block (BB) and condition coverage (CC):

Source file BLAST (BB) BB CC
#cases Time[s] #cases Time[s] Min* #cases Time[s]
kbfiltr.i 39 300 26 18 6 98 24
floppy.i 111 1500 63 1041 10 175 1259
cdaudio.i 85 1500 71 1240 7 161 1243
parport.i 213 5460 134 1859 21 351 2915
parclass.i 219 2520 156 1324 16 392 2070
matlab.c 5 30 1 16 31
statemate.c 17 12 0 63 16
nsichneu.c 14 3402 19 274 6929
adpcm.c 1 34 0 9 36
autopilot.i 206 894 14 450 1358
fly_by_wire.i 4 89 1 7 113

*: Number of test cases removed by our test suite minimization algorithm.

To demonstrate the power of our approach,we considered queries on autopilot.i that
enforce a certain function call stack and focus coverage criteria to single functions:

@entry -> / & @entry -> / & @entry -> @exit

queries for a test suite satisfying coverage criteria , where all test cases
start in periodic task passing its entry, thereafter the entry of , the entry
of and finally an exitpoint of periodic task. The following table shows the results.
The last two coverage criteria combine basic block and condition coverage at different
locations in the source code.

 =/@blocks #cases Time[s] Min course_run course_pid_run 171 1067 14 climb_control_task climb_pid_run 169 968 7 altitude_control_task altitude_pid_run 170 936 11 =/@conditions #cases Time[s] Min course_run course_pid_run 369 2283 – climb_control_task climb_pid_run 361 2422 – altitude_control_task altitude_pid_run 365 2155 – =/@blocks,/@conditions #cases Time[s] Min course_run course_pid_run 377 1563 0 climb_control_task climb_pid_run 359 1625 0 altitude_control_task altitude_pid_run 372 1428 0 =/@conditions,/@blocks #cases Time[s] Min course_run course_pid_run 170 1436 14 climb_control_task climb_pid_run 174 1138 12 altitude_control_task altitude_pid_run 174 921 14

## 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.

## FRIDA’17 at DISC

We have a great program at FRIDA’17 that takes place in Vienna

## Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30.