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
adpcm.c 365
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).

[2] http://www.mrtc.mdh.se/projects/wcet/benchmarks.html

[3] http://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=97

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.

-: No results from BLAST available.

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:

  > in periodic_task/ cover  passing
    @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

Latest News

FORSYTE organizes CAV 2018

The FORSYTE group is co-organizing the 30th International Conference on Computer Aided Verification (CAV), which will take place in Oxford from July 14-17, 2018, as part of the Federated Logic Conference (FLoC). CAV is the leading conference on theory and practice of computer-aided formal verification for hardware and software systems. The paper submission deadline is […]

Continue reading

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. Helmut unexpectedly passed away in March 2016; he was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the […]

Continue reading

Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30. The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) […]

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Full news archive