IA159 Formal Methods for Software Analysis
Verification Witnesses, SV-COMP, and Test-Comp
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
focus
verification witnesses in GraphML and YAML
competition on software verification (SV-COMP)
competition on software testing (Test-Comp)
sources
D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, T. Lemberger, and
M. Tautschnig: Verification Witnesses, ACM TOSEM 2022.
P. Ayaziová, D. Beyer, M. Lingsch-Rosenfeld, M. Spiessl, and J. Strejˇcek:
Software Verification Witnesses 2.0, SPIN 2024.
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 2/56
Motivation
verification tools contain bugs
72 verifiers participated in the Overall category of SV-COMP 2018-2023
How many provided only valid results?
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 3/56
Motivation
verification tools contain bugs
72 verifiers participated in the Overall category of SV-COMP 2018-2023
How many provided only valid results? Only 6!
2 out of 17 in SV-COMP 2024
verification result should be accompanied by a witness
witness can be checked by independent witness validators
=⇒ witness format needed
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 4/56
Motivation
verification tools contain bugs
72 verifiers participated in the Overall category of SV-COMP 2018-2023
How many provided only valid results? Only 6!
2 out of 17 in SV-COMP 2024
verification result should be accompanied by a witness
witness can be checked by independent witness validators
=⇒ witness format needed
checking witness validity should be easier than deciding the verification task
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 5/56
Verification tasks and properties
verification task is a pair of
program to be verified (usually in source code)
property to be verified
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 6/56
Verification tasks and properties
verification task is a pair of
program to be verified (usually in source code)
property to be verified
common properties
reachability safety
error locations/functions are unreachable
many specific properties can be reduced to this:
division by zero, assertion checking, . . .
memory safety
no invalid pointer dereference, no invalid deallocation, no memory leaks
no signed integer overflow
program termination
no data race, . . .
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 7/56
Violation witnesses
a violation witness represents property violation, i.e., some program execution
violating the property
witnesses representing only the violating execution would be big and hard to
validate as they have to represent
values of all inputs
interaction with environment
thread scheduling
program non-determinism
order of evaluation of subexpressions: f(x) + g(y)
addresses of allocations: p = malloc(10)
. . .
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 8/56
Example of program nondeterminism
1 int g = 0;
2
3 int f1() {
4 g = 2 * g;
5 return 5;
6 }
7
8 int f2() {
9 g++;
10 return 7;
11 }
12
13 int h() {
14 return f1() + f2();
15 }
16
17 int main() {
18 int c = h() + h();
19 \\ what is the value of g here?
20 }
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 9/56
Example of program nondeterminism
1 int g = 0;
2
3 int f1() {
4 g = 2 * g;
5 return 5;
6 }
7
8 int f2() {
9 g++;
10 return 7;
11 }
12
13 int h() {
14 return f1() + f2();
15 }
16
17 int main() {
18 int c = h() + h();
19 \\ what is the value of g here?
20 }
3
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 10/56
Example of program nondeterminism
1 int g = 0;
2
3 int f1() {
4 g = 2 * g;
5 return 5;
6 }
7
8 int f2() {
9 g++;
10 return 7;
11 }
12
13 int h() {
14 return f1() + f2();
15 }
16
17 int main() {
18 int c = h() + h();
19 \\ what is the value of g here?
20 }
3, 6
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 11/56
Example of program nondeterminism
1 int g = 0;
2
3 int f1() {
4 g = 2 * g;
5 return 5;
6 }
7
8 int f2() {
9 g++;
10 return 7;
11 }
12
13 int h() {
14 return f1() + f2();
15 }
16
17 int main() {
18 int c = h() + h();
19 \\ what is the value of g here?
20 }
3, 6, 4, 5
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 12/56
Violation witnesses
a violation witness represents property violation, i.e., some program execution
violating the property
witnesses representing only the violating execution would be big and hard to
validate as they have to represent
values of all inputs
interaction with environment
thread scheduling
program non-determinism
order of evaluation of subexpressions: f(x) + g(y)
addresses of allocations: p = malloc(10)
. . .
=⇒ a violation witness can represent more executions
it is considered valid if at least one of the represented executions violates the
property
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 13/56
Correctness witnesses
a correctness witness provides arguments that the program is correct
it provides invariants for some locations
it is considered valid if
1 all the provided invariants are indeed invariants and
2 the program satisfies the property
witness validity does not depend on the relevance of the invariants in the
witness to the property satisfaction
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 14/56
Witness format 1.0
aka GraphML witness format
GraphML witness format aka witness format 1.0
based on automata represented in GraphML
format for violation witnesses introduced in 2015
correctness witnesses added in 2016
semantics defined in terms of control flow automata (CFA)
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 16/56
GraphML witness format aka witness format 1.0
based on automata represented in GraphML
format for violation witnesses introduced in 2015
correctness witnesses added in 2016
semantics defined in terms of control flow automata (CFA)
witness automaton
a nondeterministic finite automaton accepting a set of program executions
each edge is labelled with a pair (S, ψ) of
a source-code guard S representing a subset of CFA edges
a state-space guard ψ restricting the state space
states are labelled with invariants
sink states are non-accepting states without any successor
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 17/56
Source-code guards
startline: x matches CFA edges that begin at line x
endline: x matches CFA edges that end at line x
startoffset: x matches CFA edges that start at column x
endoffset: x matches CFA edges that end at column x
control: true/false matches CFA edges entering true/false branch of a
branching statement
enterFunction: name matches calls of function name
returnFromFunction: name matches returns from name
enterLoopHead matches CFA edges entering a loop head (in CFA sense)
support for concurrent programs: threadId and createThread
an edge can contain more guards (all restrictions apply)
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 18/56
State-space guards
assumption: φ
says that φ holds in the execution state immediately after the automaton edge
is passed
φ is an expression that
evaluates to a Boolean type or equivalent (int in C)
cannot contain function calls and cannot have any side-effects
can use only program variables and \result
\result refers to the return value from the function given by
assumption.resultfunction
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 19/56
Implicit loop edges
each non-sink state q has an implicit otherwise (o/w) loop with
source-code guard that corresponds to all CFA edges not matched by explicit
edges of q and
q
. . .(S1, ψ1) (S2, ψ2) (Sk , ψk )
o/w CFA edges not in S1 ∪ S2 ∪ . . . ∪ Sk
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 20/56
Implicit loop edges
each non-sink state q has an implicit otherwise (o/w) loop with
source-code guard that corresponds to all CFA edges not matched by explicit
edges of q and
q
. . .(S1, ψ1) (S2, ψ2) (Sk , ψk )
o/w CFA edges not in S1 ∪ S2 ∪ . . . ∪ Sk
state-space guard true
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 21/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 22/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0
q1
qE
4, enterFunction(main):
o/w
o/w
o/w
q2
q3
5, n = 2:
13, v = 224:
o/w
13, v = 63:
o/w
a label S : φ is an abbreviation for (S, φ)
assumptions true are omitted
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 23/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0
q1
qE
4, enterFunction(main):
o/w
o/w
o/w
q2
q3
5, n = 2:
13, v = 224:
o/w
13, v = 63:
o/w
represents 1 violating execution
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 24/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0
q1
qE
4, enterFunction(main):
o/w
o/w
o/w
5, n = 2:
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 25/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0
q1
qE
4, enterFunction(main):
o/w
o/w
o/w
5, n = 2:
represents violating and non-violating executions
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 26/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0
q1
q2q3
q4
qE1
q⊥1
q⊥2
4, enterFunction(main):
o/w
6,true:
11, enterLoopHead:
o/w
12, false:
12, true:
o/w
15, enterLoopHead:
o/w
17, true:
17, false:
o/w
o/w
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 27/56
Violation witnesses
no invariants in automata states (true by default)
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned char s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0
q1
q2q3
q4
qE1
q⊥1
q⊥2
4, enterFunction(main):
o/w
6,true:
11, enterLoopHead:
o/w
12, false:
12, true:
o/w
15, enterLoopHead:
o/w
17, true:
17, false:
o/w
o/w
valid, but not very useful witness
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 28/56
Correctness witnesses
have to accept all executions, no sink nodes
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned int s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 29/56
Correctness witnesses
have to accept all executions, no sink nodes
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned int s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
q0true
q1true
q2
s ≤ i · 255
∧ 0 ≤ i ≤ 255
∧ n ≤ 255
q3true q4 true
4, enterFunction(main):
o/w
11, enterLoopHead:
o/w
o/w
12, true: 12, false:
o/w
15, enterLoopHead:
o/w
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 30/56
Notes
witnesses contain also metadata about
the corresponding verification task
the witnessed verification result
producer of the witness
considered architecture (32-bit or 64-bit)
creation time
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 31/56
Notes
witnesses contain also metadata about
the corresponding verification task
the witnessed verification result
producer of the witness
considered architecture (32-bit or 64-bit)
creation time
successes and fails of the GraphML format
+ widely accepted by the community
+ improved the quality of verification tools
+ other applications, e.g., cooperative verification
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 32/56
Notes
witnesses contain also metadata about
the corresponding verification task
the witnessed verification result
producer of the witness
considered architecture (32-bit or 64-bit)
creation time
successes and fails of the GraphML format
+ widely accepted by the community
+ improved the quality of verification tools
+ other applications, e.g., cooperative verification
− witness validators do not support all features of the format
ignoring unsupported features may lead to incorrect verdict
− verifiers do not use the whole power of the format
− semantics given on CFA, but translation to CFA is ambiguous
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 33/56
Witness format 2.0
aka YAML witness format
Witness format 2.0
design goals
clear semantics on source code
validators that fully implement the format needed
=⇒ as simple as possible
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 35/56
Witness format 2.0
design goals
clear semantics on source code
validators that fully implement the format needed
=⇒ as simple as possible
design decisions
start with the support of the most common properties and sequential
programs and then extend it
use YAML
correctness witnesses specify invariants with the corresponding program
locations
violation witnesses describe executions with use of waypoints
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 36/56
Waypoints
waypoint = basic element of witnesses
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 37/56
Waypoints
waypoint = basic element of witnesses
each waypoint has 4 aspects:
action - the role within the witness
location - code location the waypoint is associated to
file_name
file_hash (optional)
line
column (optional, the default is the first suitable column)
type - the type of constraint it puts on runs
constraint - the constraint itself
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 38/56
Waypoint types
1 assumption
location: before a statement
constraint: a side-effect-free expression
for example x[5] > z + 5 or ptr != NULL
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 39/56
Waypoint types
1 assumption
location: before a statement
constraint: a side-effect-free expression
for example x[5] > z + 5 or ptr != NULL
2 branching
location: branching keyword like if, while, . . .
constraint: true or false
specific support for switch statements
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 40/56
Waypoint types
1 assumption
location: before a statement
constraint: a side-effect-free expression
for example x[5] > z + 5 or ptr != NULL
2 branching
location: branching keyword like if, while, . . .
constraint: true or false
specific support for switch statements
3 function_enter
location: the right parenthesis of the function call foo()
constraint: has to be omitted
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 41/56
Waypoint types
1 assumption
location: before a statement
constraint: a side-effect-free expression
for example x[5] > z + 5 or ptr != NULL
2 branching
location: branching keyword like if, while, . . .
constraint: true or false
specific support for switch statements
3 function_enter
location: the right parenthesis of the function call foo()
constraint: has to be omitted
4 function_return
location: the right parenthesis of the function call foo()
constraint: \result op const, where op ∈ {==, ! =, <=, . . .} and const is a
constant expression
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 42/56
Waypoint types
1 assumption
location: before a statement
constraint: a side-effect-free expression
for example x[5] > z + 5 or ptr != NULL
2 branching
location: branching keyword like if, while, . . .
constraint: true or false
specific support for switch statements
3 function_enter
location: the right parenthesis of the function call foo()
constraint: has to be omitted
4 function_return
location: the right parenthesis of the function call foo()
constraint: \result op const, where op ∈ {==, ! =, <=, . . .} and const is a
constant expression
5 target
location: the statement that violates the property
constraint: has to be omitted
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 43/56
Waypoint actions
W follow - the waypoint has to be passed as soon as the location is
entered
W avoid - the run represented by the witness must not pass the
waypoint (“sink node”)
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 44/56
Waypoint actions
W follow - the waypoint has to be passed as soon as the location is
entered
W avoid - the run represented by the witness must not pass the
waypoint (“sink node”)
W - follow waypoint of type target
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 45/56
Segments
sequence of 0+ avoid waypoints ended by 1 follow or target waypoint
segments ended by a follow waypoint are normal segments
segments ended by a target waypoint are final segments
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 46/56
Segments
sequence of 0+ avoid waypoints ended by 1 follow or target waypoint
segments ended by a follow waypoint are normal segments
segments ended by a target waypoint are final segments
a part of an execution matches a normal segment if
the part ends by its first visit of the follow waypoint location and the constraint
holds in this moment
no avoid waypoint is passed (constraint is valid at the corresponding location)
until that
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 47/56
Segments
sequence of 0+ avoid waypoints ended by 1 follow or target waypoint
segments ended by a follow waypoint are normal segments
segments ended by a target waypoint are final segments
a part of an execution matches a normal segment if
the part ends by its first visit of the follow waypoint location and the constraint
holds in this moment
no avoid waypoint is passed (constraint is valid at the corresponding location)
until that
an execution matches a witness if
it has a prefix that can be divided into parts that match the corresponding
normal segments
the rest does not pass any avoid waypoint of the final segment
it violates the specified property by the target statement
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 48/56
Witness example
start
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 49/56
Witness example
start
normalsegmentsfinal
segment
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 50/56
Witness example
start
example.c, line 22
assumption x >= 1024U
example.c, line 35
branching false
example.c, line 28
function_enter
example.c, line 152
function_return \result == 10
example.c, line 35
branching false
example.c, line 350
assumption ptr != NULL
example.c, line 819
target
normalsegmentsfinal
segment
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 51/56
Witness example - YAML notation
example.c, line 35
branching false
example.c, line 28
function_enter
example.c, line 152
function_return \result == 10
- segment:
- waypoint:
action: avoid
type: branching
location:
file_name: example.c
line: 35
constraint:
value: false
- waypoint:
action: avoid
type: function_enter
location:
file_name: example.c
line: 28
- waypoint:
action: follow
type: function_return
location:
file_name: example.c
line: 152
constraint:
value: \result == 10
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 52/56
Correctness witnesses
1 void reach_error(){}
2 extern unsigned char __nondet_uchar(void);
3
4 int main() {
5 unsigned char n = __nondet_uchar();
6 if (n == 0) {
7 return 0;
8 }
9 unsigned char v = 0;
10 unsigned int s = 0;
11 unsigned int i = 0;
12 while (i < n) {
13 v = __nondet_uchar();
14 s += v;
15 ++i;
16 }
17 if (s < v) {
18 reach_error();
19 return 1;
20 }
21 return 0;
22 }
- entry_type: invariant_set
metadata: <...>
content:
- invariant:
type: loop_invariant
location:
file_name: "inv-a.c"
line: 12
column: 1
function: main
value: "s <= i*255 && 0 <= i && i <= 255 && n <= 255"
format: c_expression
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 53/56
Notes
witness format 2.0
published in 2024
increasing number of verifiers and validators supporting the format
better interoperability compared to the old format
a bit less expressive than the old format
should be the new standard of SV-COMP in several years
needs to be extended to support
parallel programs
correctness witnesses for memory safety
violation and correctness witnesses of termination
. . .
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 54/56
Competition on Software Verification: SV-COMP
running every year since 2012
very popular and growing repository of C and Java verification tasks marked
with expected results
scoring schema
1 point for finding a program bug (if witness is validated)
2 points for proving correctness (if witness is validated)
-16 points for reporting bug in a correct program (false alarm)
-32 points for claiming correctness of an incorrect program (false negative)
points in the overall score are weighted by category sizes
graphs indicate winners, speed, sequential portfolio of algorithms in tools, the
number of incorrect answers, programming language of tools, . . .
https://sv-comp.sosy-lab.org
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 55/56
Competition on Software Testing: Test-Comp
running every year since 2019
uses the same benchmarks as SV-COMP
the goal is to generate a test suit that
finds an error (category Cover-Error), benchmarks are programs with an error
has a high branch coverage (category Cover-Branches)
https://test-comp.sosy-lab.org
IA159 Formal Methods for Software Analysis: Verification Witnesses, SV-COMP, and Test-Comp 56/56