Termination-Portal.org - User contributions [en]

C Programs

2015-07-29T15:05:26Z

Cryingshadow: format fix

[[Category:Categories]]

== Proposed semantics ==

* The starting point is the main function without arguments.

* Functions which are only declared, but not defined, are considered to be terminating, have no side effects, and return a non-deterministic value according to the function's return type.

* The special (and only declared) function __VERIFIER_nondet_String() returns a non-deterministic C String, i.e., a pointer to some freshly allocated memory where the last byte of this allocation is the value '\0' (we may provide a standard implementation for this function, but provers are allowed to hard-code its semantics).

* In C, memory-unsafe programs can behave arbitrarily. Therefore, neither YES nor NO is a correct result for programs violating memory safety. So a proof of memory safety needs to be part of a termination proof. If there is interest for that, we could also offer an additional category where memory safety can be assumed and where no programs are allowed which might violate memory safety.

* We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.

* Integer division by negative numbers is assumed to be done by truncation towards zero (as in the C99 standard and no implementation-defined behavior as in the C89 standard).

* We assume that allocation of memory always succeeds, i.e., alloca and malloc never return null pointers and allocation of constant size arrays cannot lead to undefined behavior. Moreover, read access to allocated, but uninitialized memory is assumed to just return a non-deterministic value.

* We assume the following sizes of primitive data types:
bool: 8 bit
char: 8 bit
short: 16 bit
int: 32 bit
long: 64 bit
float: 32 bit
double: 64 bit
pointer: 64 bit

* Programs where the evaluation order of operations is not defined according to the C standard and where different execution orders of the operations lead to different resulting states are not allowed. As an example, the program
int main(){
int x = 0;
while( x++ == x );
}
: is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <code>P</code> where the execution of <code>gcc -c -std=c99 -Wsequence-point P</code> shows a warning.

* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).

* Time limit: 300 seconds.

== See also ==

Section D. of [http://sv-comp.sosy-lab.org/2014/demo.php Termination Competition on Software Verification (SV-COMP)]

C Programs

2015-07-29T15:04:54Z

Cryingshadow: formatting

[[Category:Categories]]

== Proposed semantics ==

* The starting point is the main function without arguments.

* Functions which are only declared, but not defined, are considered to be terminating, have no side effects, and return a non-deterministic value according to the function's return type.

* The special (and only declared) function __VERIFIER_nondet_String() returns a non-deterministic C String, i.e., a pointer to some freshly allocated memory where the last byte of this allocation is the value '\0' (we may provide a standard implementation for this function, but provers are allowed to hard-code its semantics).

* In C, memory-unsafe programs can behave arbitrarily. Therefore, neither YES nor NO is a correct result for programs violating memory safety. So a proof of memory safety needs to be part of a termination proof. If there is interest for that, we could also offer an additional category where memory safety can be assumed and where no programs are allowed which might violate memory safety.

* We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.

* Integer division by negative numbers is assumed to be done by truncation towards zero (as in the C99 standard and no implementation-defined behavior as in the C89 standard).

* We assume that allocation of memory always succeeds, i.e., alloca and malloc never return null pointers and allocation of constant size arrays cannot lead to undefined behavior. Moreover, read access to allocated, but uninitialized memory is assumed to just return a non-deterministic value.

* We assume the following sizes of primitive data types:
bool: 8 bit
char: 8 bit
short: 16 bit
int: 32 bit
long: 64 bit
float: 32 bit
double: 64 bit
pointer: 64 bit

* Programs where the evaluation order of operations is not defined according to the C standard and where different execution orders of the operations lead to different resulting states are not allowed. As an example, the program
int main(){
int x = 0;
while( x++ == x );
}
: is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <code><P></code> where the execution of <code>gcc -c -std=c99 -Wsequence-point <P></code> shows a warning.

* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).

* Time limit: 300 seconds.

== See also ==

Section D. of [http://sv-comp.sosy-lab.org/2014/demo.php Termination Competition on Software Verification (SV-COMP)]

C Programs

2015-07-29T15:00:22Z

Cryingshadow: new rules according to discussion on termtools

[[Category:Categories]]

== Proposed semantics ==

* The starting point is the main function without arguments.

* Functions which are only declared, but not defined, are considered to be terminating, have no side effects, and return a non-deterministic value according to the function's return type.

* The special (and only declared) function __VERIFIER_nondet_String() returns a non-deterministic C String, i.e., a pointer to some freshly allocated memory where the last byte of this allocation is the value '\0' (we may provide a standard implementation for this function, but provers are allowed to hard-code its semantics).

* In C, memory-unsafe programs can behave arbitrarily. Therefore, neither YES nor NO is a correct result for programs violating memory safety. So a proof of memory safety needs to be part of a termination proof. If there is interest for that, we could also offer an additional category where memory safety can be assumed and where no programs are allowed which might violate memory safety.

* We assume integers to be mathematical integers, i.e., over- or underflows cannot occur. If there is interest for that, we could also offer an additional category where overflows of unsigned integers are treated as two's complement overflows and where neither YES nor NO is a correct result for programs with overflows of signed integers.

* Integer division by negative numbers is assumed to be done by truncation towards zero (as in the C99 standard and no implementation-defined behavior as in the C89 standard).

* We assume that allocation of memory always succeeds, i.e., alloca and malloc never return null pointers and allocation of constant size arrays cannot lead to undefined behavior. Moreover, read access to allocated, but uninitialized memory is assumed to just return a non-deterministic value.

* We assume the following sizes of primitive data types:
bool: 8 bit
char: 8 bit
short: 16 bit
int: 32 bit
long: 64 bit
float: 32 bit
double: 64 bit
pointer: 64 bit

* Programs where the evaluation order of operations is not defined according to the C standard and where different execution orders of the operations lead to different resulting states are not allowed. As an example, the program

int main(){
int x = 0;
while( x++ == x );
}

is not allowed since the evaluation order between ++ and == is not defined according to the C standard and if ++ is evaluated first, the program terminates whereas it does not if == is evaluated first. To enable an automatic check for such programs, we disallow all programs <P> where the execution of gcc -c -std=c99 -Wsequence-point <P> shows a warning.

* The scoring should be the same as in all other categories (proving termination or non-termination both gives 1 point and there will be a penalty for wrong answers).

* Time limit: 300 seconds.

== See also ==

Section D. of [http://sv-comp.sosy-lab.org/2014/demo.php Termination Competition on Software Verification (SV-COMP)]

C Integer Programs

2015-07-06T17:36:50Z

Cryingshadow: parse expressions from left to right when there are no parantheses

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we introduce a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following ANTLR grammar, which can also be used to automatically build a parser:

/* Type: ANTLR
* Title: Grammar for C Integer Programs
* Description: A grammar definiton for C integer programs
* Project: AProVE
* Authors: Thomas Ströder
* Copyright: Copyright (c) 2015
* Department: RWTH Aachen / Templergraben 55 / D-52056 Aachen
*
* The following license text is based on the "BSD licence".
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions
* are met:
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
* 3. The name of the author may not be used to endorse or promote products
* derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
* IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
* OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
* IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
* NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
* THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/

grammar IntProg;

// parser rules

nondet : NONDETNAME W* OPENP W* CLOSEP;

num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;

mult_expr : num_atom (W* MULT W* num_atom)*;

num_expr : mult_expr (W* (PLUS | MINUS) W* mult_expr)* | MINUS W* mult_expr (W* (PLUS | MINUS) W* mult_expr)*;

bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;

and_expr : bool_atom (W* AND W* bool_atom)*;

bool_expr : and_expr (W* OR W* and_expr)* | NOT W* bool_atom;

loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

condition :
IF
W*
OPENP W* bool_expr W* CLOSEP
W*
OPENC W* (instructions W*)? CLOSEC
(W* ELSE W* OPENC W* (instructions W*)? CLOSEC)?;

assignment : V W* ASSIGN W* num_expr W* TERMINATOR;

instruction : loop | condition | assignment;

declaration : INT W+ V (W* COMMA W* V)* W* TERMINATOR;

declarations : declaration (W* declarations)?;

instructions : instruction (W* instructions)?;

// the opening part of each program
// ("typedef enum {false,true} bool;extern int __VERIFIER_nondet_int(void);int main(){")
pre :
W*
TYPEDEF W+ ENUM W* OPENC W* FALSE W* COMMA W* TRUE W* CLOSEC W* BOOL W* TERMINATOR
W*
EXTERN W+ INT W+ NONDETNAME W* OPENP W* VOID W* CLOSEP W* TERMINATOR
W*
INT W+ MAIN W* OPENP W* CLOSEP W* OPENC;

// the closing part of each program ("return 0;}")
post : RETURN W+ ZERO W* TERMINATOR W* CLOSEC W*;

program : pre (W* declarations)? (W* instructions)? W* post;

// lexer rules

INT : 'int';
IF : 'if';
WHILE : 'while';
ELSE : 'else';
TERMINATOR : ';';
OPENP : '(';
CLOSEP : ')';
OPENC : '{';
CLOSEC : '}';
MULT : '*';
MINUS : '-';
PLUS : '+';
BO : '<=' | '>=' | '<' | '>' | '==' | '!=';
ASSIGN : '=';
NONDETNAME : '__VERIFIER_nondet_int';
OR : '||';
AND : '&&';
NOT : '!';
TRUE : 'true';
FALSE : 'false';
TYPEDEF : 'typedef';
ENUM : 'enum';
COMMA : ',';
BOOL : 'bool';
EXTERN : 'extern';
VOID : 'void';
MAIN : 'main';
RETURN : 'return';
ZERO : '0';
POSITIVE : NONZERO DIGIT*;
fragment NONZERO : '1'..'9';
fragment DIGIT : ZERO | NONZERO;
V : CHAR ALPHANUM*;
fragment ALPHANUM : CHAR | DIGIT;
fragment CHAR : LOW | UP;
fragment LOW : 'a'..'z';
fragment UP: 'A'..'Z';
W : ' ' | '\n' | '\r' | '\t';
BLOCKCOMMENT : '/*' (.)* '*/' {$channel=HIDDEN;};
LINECOMMENT : '//' (~('\r'|'\n'))* {$channel=HIDDEN;};

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used. So while the grammar above allows, e.g., nesting of boolean expressions inside arithmetic expressions (to make the automated generation of a parser easier), such programs have no defined semantics and are excluded from benchmarks for the competition.

C Integer Programs

2015-07-06T16:51:24Z

Cryingshadow: allow negative mutliplicative expressions

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we introduce a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following ANTLR grammar, which can also be used to automatically build a parser:

/* Type: ANTLR
* Title: Grammar for C Integer Programs
* Description: A grammar definiton for C integer programs
* Project: AProVE
* Authors: Thomas Ströder
* Copyright: Copyright (c) 2015
* Department: RWTH Aachen / Templergraben 55 / D-52056 Aachen
*
* The following license text is based on the "BSD licence".
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions
* are met:
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
* 3. The name of the author may not be used to endorse or promote products
* derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
* IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
* OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
* IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
* NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
* THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/

grammar IntProg;

// parser rules

nondet : NONDETNAME W* OPENP W* CLOSEP;

num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;

mult_expr : num_atom (W* MULT W* mult_expr)?;

num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* mult_expr;

bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;

and_expr : bool_atom (W* AND W* and_expr)?;

bool_expr : and_expr (W* OR W* bool_expr)? | NOT W* bool_atom;

loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

condition :
IF
W*
OPENP W* bool_expr W* CLOSEP
W*
OPENC W* (instructions W*)? CLOSEC
(W* ELSE W* OPENC W* (instructions W*)? CLOSEC)?;

assignment : V W* ASSIGN W* num_expr W* TERMINATOR;

instruction : loop | condition | assignment;

declaration : INT W+ V (W* COMMA W* V)* W* TERMINATOR;

declarations : declaration (W* declarations)?;

instructions : instruction (W* instructions)?;

// the opening part of each program
// ("typedef enum {false,true} bool;extern int __VERIFIER_nondet_int(void);int main(){")
pre :
W*
TYPEDEF W+ ENUM W* OPENC W* FALSE W* COMMA W* TRUE W* CLOSEC W* BOOL W* TERMINATOR
W*
EXTERN W+ INT W+ NONDETNAME W* OPENP W* VOID W* CLOSEP W* TERMINATOR
W*
INT W+ MAIN W* OPENP W* CLOSEP W* OPENC;

// the closing part of each program ("return 0;}")
post : RETURN W+ ZERO W* TERMINATOR W* CLOSEC W*;

program : pre (W* declarations)? (W* instructions)? W* post;

// lexer rules

INT : 'int';
IF : 'if';
WHILE : 'while';
ELSE : 'else';
TERMINATOR : ';';
OPENP : '(';
CLOSEP : ')';
OPENC : '{';
CLOSEC : '}';
MULT : '*';
MINUS : '-';
PLUS : '+';
BO : '<=' | '>=' | '<' | '>' | '==' | '!=';
ASSIGN : '=';
NONDETNAME : '__VERIFIER_nondet_int';
OR : '||';
AND : '&&';
NOT : '!';
TRUE : 'true';
FALSE : 'false';
TYPEDEF : 'typedef';
ENUM : 'enum';
COMMA : ',';
BOOL : 'bool';
EXTERN : 'extern';
VOID : 'void';
MAIN : 'main';
RETURN : 'return';
ZERO : '0';
POSITIVE : NONZERO DIGIT*;
fragment NONZERO : '1'..'9';
fragment DIGIT : ZERO | NONZERO;
V : CHAR ALPHANUM*;
fragment ALPHANUM : CHAR | DIGIT;
fragment CHAR : LOW | UP;
fragment LOW : 'a'..'z';
fragment UP: 'A'..'Z';
W : ' ' | '\n' | '\r' | '\t';
BLOCKCOMMENT : '/*' (.)* '*/' {$channel=HIDDEN;};
LINECOMMENT : '//' (~('\r'|'\n'))* {$channel=HIDDEN;};

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used. So while the grammar above allows, e.g., nesting of boolean expressions inside arithmetic expressions (to make the automated generation of a parser easier), such programs have no defined semantics and are excluded from benchmarks for the competition.

C Integer Programs

2015-07-06T16:21:58Z

Cryingshadow: allow chaining of expressions without parantheses (e.g., 1 + 1 + 1 instead of 1 + (1 + 1))

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we introduce a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following ANTLR grammar, which can also be used to automatically build a parser:

/* Type: ANTLR
* Title: Grammar for C Integer Programs
* Description: A grammar definiton for C integer programs
* Project: AProVE
* Authors: Thomas Ströder
* Copyright: Copyright (c) 2015
* Department: RWTH Aachen / Templergraben 55 / D-52056 Aachen
*
* The following license text is based on the "BSD licence".
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions
* are met:
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
* 3. The name of the author may not be used to endorse or promote products
* derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
* IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
* OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
* IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
* NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
* THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/

grammar IntProg;

// parser rules

nondet : NONDETNAME W* OPENP W* CLOSEP;

num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;

mult_expr : num_atom (W* MULT W* mult_expr)?;

num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* num_atom;

bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;

and_expr : bool_atom (W* AND W* and_expr)?;

bool_expr : and_expr (W* OR W* bool_expr)? | NOT W* bool_atom;

loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

condition :
IF
W*
OPENP W* bool_expr W* CLOSEP
W*
OPENC W* (instructions W*)? CLOSEC
(W* ELSE W* OPENC W* (instructions W*)? CLOSEC)?;

assignment : V W* ASSIGN W* num_expr W* TERMINATOR;

instruction : loop | condition | assignment;

declaration : INT W+ V (W* COMMA W* V)* W* TERMINATOR;

declarations : declaration (W* declarations)?;

instructions : instruction (W* instructions)?;

// the opening part of each program
// ("typedef enum {false,true} bool;extern int __VERIFIER_nondet_int(void);int main(){")
pre :
W*
TYPEDEF W+ ENUM W* OPENC W* FALSE W* COMMA W* TRUE W* CLOSEC W* BOOL W* TERMINATOR
W*
EXTERN W+ INT W+ NONDETNAME W* OPENP W* VOID W* CLOSEP W* TERMINATOR
W*
INT W+ MAIN W* OPENP W* CLOSEP W* OPENC;

// the closing part of each program ("return 0;}")
post : RETURN W+ ZERO W* TERMINATOR W* CLOSEC W*;

program : pre (W* declarations)? (W* instructions)? W* post;

// lexer rules

INT : 'int';
IF : 'if';
WHILE : 'while';
ELSE : 'else';
TERMINATOR : ';';
OPENP : '(';
CLOSEP : ')';
OPENC : '{';
CLOSEC : '}';
MULT : '*';
MINUS : '-';
PLUS : '+';
BO : '<=' | '>=' | '<' | '>' | '==' | '!=';
ASSIGN : '=';
NONDETNAME : '__VERIFIER_nondet_int';
OR : '||';
AND : '&&';
NOT : '!';
TRUE : 'true';
FALSE : 'false';
TYPEDEF : 'typedef';
ENUM : 'enum';
COMMA : ',';
BOOL : 'bool';
EXTERN : 'extern';
VOID : 'void';
MAIN : 'main';
RETURN : 'return';
ZERO : '0';
POSITIVE : NONZERO DIGIT*;
fragment NONZERO : '1'..'9';
fragment DIGIT : ZERO | NONZERO;
V : CHAR ALPHANUM*;
fragment ALPHANUM : CHAR | DIGIT;
fragment CHAR : LOW | UP;
fragment LOW : 'a'..'z';
fragment UP: 'A'..'Z';
W : ' ' | '\n' | '\r' | '\t';
BLOCKCOMMENT : '/*' (.)* '*/' {$channel=HIDDEN;};
LINECOMMENT : '//' (~('\r'|'\n'))* {$channel=HIDDEN;};

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used. So while the grammar above allows, e.g., nesting of boolean expressions inside arithmetic expressions (to make the automated generation of a parser easier), such programs have no defined semantics and are excluded from benchmarks for the competition.

C Integer Programs

2015-07-06T09:44:55Z

Cryingshadow: also allow comments

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we introduce a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following ANTLR grammar, which can also be used to automatically build a parser:

/* Type: ANTLR
* Title: Grammar for C Integer Programs
* Description: A grammar definiton for C integer programs
* Project: AProVE
* Authors: Thomas Ströder
* Copyright: Copyright (c) 2015
* Department: RWTH Aachen / Templergraben 55 / D-52056 Aachen
*
* The following license text is based on the "BSD licence".
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions
* are met:
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
* 3. The name of the author may not be used to endorse or promote products
* derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
* IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
* OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
* IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
* NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
* THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/

grammar IntProg;

// parser rules

nondet : NONDETNAME W* OPENP W* CLOSEP;

num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;

mult_expr : num_atom (W* MULT W* num_atom)?;

num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* num_atom;

bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;

and_expr : bool_atom (W* AND W* bool_atom)?;

bool_expr : and_expr (W* OR W* and_expr)? | NOT W* bool_atom;

loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

condition :
IF
W*
OPENP W* bool_expr W* CLOSEP
W*
OPENC W* (instructions W*)? CLOSEC
(W* ELSE W* OPENC W* (instructions W*)? CLOSEC)?;

assignment : V W* ASSIGN W* num_expr W* TERMINATOR;

instruction : loop | condition | assignment;

declaration : INT W+ V (W* COMMA W* V)* W* TERMINATOR;

declarations : declaration (W* declarations)?;

instructions : instruction (W* instructions)?;

// the opening part of each program
// ("typedef enum {false,true} bool;extern int __VERIFIER_nondet_int(void);int main(){")
pre :
W*
TYPEDEF W+ ENUM W* OPENC W* FALSE W* COMMA W* TRUE W* CLOSEC W* BOOL W* TERMINATOR
W*
EXTERN W+ INT W+ NONDETNAME W* OPENP W* VOID W* CLOSEP W* TERMINATOR
W*
INT W+ MAIN W* OPENP W* CLOSEP W* OPENC;

// the closing part of each program ("return 0;}")
post : RETURN W+ ZERO W* TERMINATOR W* CLOSEC W*;

program : pre (W* declarations)? (W* instructions)? W* post;

// lexer rules

INT : 'int';
IF : 'if';
WHILE : 'while';
ELSE : 'else';
TERMINATOR : ';';
OPENP : '(';
CLOSEP : ')';
OPENC : '{';
CLOSEC : '}';
MULT : '*';
MINUS : '-';
PLUS : '+';
BO : '<=' | '>=' | '<' | '>' | '==' | '!=';
ASSIGN : '=';
NONDETNAME : '__VERIFIER_nondet_int';
OR : '||';
AND : '&&';
NOT : '!';
TRUE : 'true';
FALSE : 'false';
TYPEDEF : 'typedef';
ENUM : 'enum';
COMMA : ',';
BOOL : 'bool';
EXTERN : 'extern';
VOID : 'void';
MAIN : 'main';
RETURN : 'return';
ZERO : '0';
POSITIVE : NONZERO DIGIT*;
fragment NONZERO : '1'..'9';
fragment DIGIT : ZERO | NONZERO;
V : CHAR ALPHANUM*;
fragment ALPHANUM : CHAR | DIGIT;
fragment CHAR : LOW | UP;
fragment LOW : 'a'..'z';
fragment UP: 'A'..'Z';
W : ' ' | '\n' | '\r' | '\t';
BLOCKCOMMENT : '/*' (.)* '*/' {$channel=HIDDEN;};
LINECOMMENT : '//' (~('\r'|'\n'))* {$channel=HIDDEN;};

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used. So while the grammar above allows, e.g., nesting of boolean expressions inside arithmetic expressions (to make the automated generation of a parser easier), such programs have no defined semantics and are excluded from benchmarks for the competition.

C Integer Programs

2015-07-03T15:29:17Z

Cryingshadow: provide ANTLR grammar to fix issues with old grammar and make it easier for other participants to build a parser

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we introduce a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following ANTLR grammar, which can also be used to automatically build a parser:

/* Type: ANTLR
* Title: Grammar for C Integer Programs
* Description: A grammar definiton for C integer programs
* Project: AProVE
* Authors: Thomas Ströder
* Copyright: Copyright (c) 2015
* Department: RWTH Aachen / Templergraben 55 / D-52056 Aachen
*
* The following license text is based on the "BSD licence".
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions
* are met:
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
* 3. The name of the author may not be used to endorse or promote products
* derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
* IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
* OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
* IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
* NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
* THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/

grammar IntProg;

// parser rules

nondet : NONDETNAME W* OPENP W* CLOSEP;

num_atom : ZERO | POS | nondet | V | OPENP W* bool_expr W* CLOSEP;

mult_expr : num_atom (W* MULT W* num_atom)?;

num_expr : mult_expr (W* (PLUS | MINUS) W* num_expr)? | MINUS W* num_atom;

bool_atom : TRUE | FALSE | num_expr (W* BO W* num_expr)?;

and_expr : bool_atom (W* AND W* bool_atom)?;

bool_expr : and_expr (W* OR W* and_expr)? | NOT W* bool_atom;

loop : WHILE W* OPENP W* bool_expr W* CLOSEP W* OPENC W* (instructions W*)? CLOSEC;

condition :
IF
W*
OPENP W* bool_expr W* CLOSEP
W*
OPENC W* (instructions W*)? CLOSEC
(W* ELSE W* OPENC W* (instructions W*)? CLOSEC)?;

assignment : V W* ASSIGN W* num_expr W* TERMINATOR;

instruction : loop | condition | assignment;

declaration : INT W+ V (W* COMMA W* V)* W* TERMINATOR;

declarations : declaration (W* declarations)?;

instructions : instruction (W* instructions)?;

// the opening part of each program
// ("typedef enum {false,true} bool;extern int __VERIFIER_nondet_int(void);int main(){")
pre :
W*
TYPEDEF W+ ENUM W* OPENC W* FALSE W* COMMA W* TRUE W* CLOSEC W* BOOL W* TERMINATOR
W*
EXTERN W+ INT W+ NONDETNAME W* OPENP W* VOID W* CLOSEP W* TERMINATOR
W*
INT W+ MAIN W* OPENP W* CLOSEP W* OPENC;

// the closing part of each program ("return 0;}")
post : RETURN W+ ZERO W* TERMINATOR W* CLOSEC W*;

program : pre (W* declarations)? (W* instructions)? W* post;

// lexer rules

INT : 'int';
IF : 'if';
WHILE : 'while';
ELSE : 'else';
TERMINATOR : ';';
OPENP : '(';
CLOSEP : ')';
OPENC : '{';
CLOSEC : '}';
MULT : '*';
MINUS : '-';
PLUS : '+';
BO : '<=' | '>=' | '<' | '>' | '==' | '!=';
ASSIGN : '=';
NONDETNAME : '__VERIFIER_nondet_int';
OR : '||';
AND : '&&';
NOT : '!';
TRUE : 'true';
FALSE : 'false';
TYPEDEF : 'typedef';
ENUM : 'enum';
COMMA : ',';
BOOL : 'bool';
EXTERN : 'extern';
VOID : 'void';
MAIN : 'main';
RETURN : 'return';
ZERO : '0';
POSITIVE : NONZERO DIGIT*;
fragment NONZERO : '1'..'9';
fragment DIGIT : ZERO | NONZERO;
V : CHAR ALPHANUM*;
fragment ALPHANUM : CHAR | DIGIT;
fragment CHAR : LOW | UP;
fragment LOW : 'a'..'z';
fragment UP: 'A'..'Z';
W : ' ' | '\n' | '\r' | '\t';

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used. So while the grammar above allows, e.g., nesting of boolean expressions inside arithmetic expressions (to make the automated generation of a parser easier), such programs have no defined semantics and are excluded from benchmarks for the competition.

C Integer Programs

2015-06-22T13:11:23Z

Cryingshadow:

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we propose a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following non-terminals:

;P
: Program
;PRE
: Start of the program, including the declaration of an external function for non-deterministic values
;POST
: The end of the program
;D
: Variable declaration
;V
: Variable name
;INS
: Instruction
;A
: Assignment
;L
: Loop
;C
: Condition
;NE
: Numerical expression
;N
: Number
;BE
: Boolean expression
;NO
: Numerical operator
;BO
: Boolean operator
;BC
: Boolean connective
;W
: Whitespace

The grammar is then (EBNF-like):
P = PRE D* W? INS* POST
PRE = W?
"extern"
W
"int"
W
"__VERIFIER_nondet_int"
W?
"("
W?
"void"
W?
")"
W?
";"
W?
"int"
W
"main"
W?
"("
W?
")"
W?
"{"
W?
POST = W? "return" W "0" W? ";" W? "}" W?
D = "int" W V W? ";"
V = [a-z,A-Z] [a-z,A-Z,0-9]*
INS = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? INS* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? INS* W? "}" (W? "else" W? "{" W? INS* W? "}")?
NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
NO = "+" | "-" | "*"
BO = "<" | ">" | "<=" | ">=" | "==" | "!="
BC = "&&" | "||" | "==" | "!="
W = (" " | "\n") (" " | "\n")*

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics is used.

C Integer Programs

2015-06-22T13:10:51Z

Cryingshadow: fix format and grammar

C Integer Programs

2015-06-22T13:08:59Z

Cryingshadow:

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we propose a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following non-terminals:

;P
: Program
;PRE
: Start of the program, including the declaration of an external function for non-deterministic values
;POST
: The end of the program
;D
: Variable declaration
;V
: Variable name
;INS
: Instruction
;A
: Assignment
;L
: Loop
;C
: Condition
;NE
: Numerical expression
;N
: Number
;BE
: Boolean expression
;NO
: Numerical operator
;BO
: Boolean operator
;BC
: Boolean connective
;W
: Whitespace

The grammar is then (EBNF-like):
P = PRE D* W? I* POST
PRE = W?
"extern"
W
"int"
W
"__VERIFIER_nondet_int"
W?
"("
W?
"void"
W?
")"
W?
";"
W?
"int"
W
"main"
W?
"("
W?
")"
W?
"{"
W?
POST = W? "return" W "0" W? ";" W? "}" W?
D = "int" W V W? ";"
V = [a-z,A-Z] [a-z,A-Z,0-9]*
I = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
NO = "+" | "-" | "*"
BO = "<" | ">" | "<=" | ">=" | "==" | "!="
BC = "&&" | "||" | "==" | "!="
W = (" " | "\n") (" " | "\n")*

Calls to <code>__VERIFIER_nondet_int()</code> yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.

C Integer Programs

2015-06-22T13:05:20Z

Cryingshadow:

[[Category:Categories]]

== Proposal ==

For the Termination Competition 2015, we propose a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

== Syntax and Semantics ==

The syntax of termination problems in this category is defined using the following non-terminals:

P:: Program
PRE:: Start of the program, including the declaration of an external function for non-deterministic values
POST:: The end of the program
D:: Variable declaration
V:: Variable name
INS:: Instruction
A:: Assignment
L:: Loop
C:: Condition
NE:: Numerical expression
N:: Number
BE:: Boolean expression
NO:: Numerical operator
BO:: Boolean operator
BC:: Boolean connective
W:: Whitespace

The grammar is then (EBNF-like):
{{{
P = PRE D* W? I* POST
PRE = W?
"extern"
W
"int"
W
"__VERIFIER_nondet_int"
W?
"("
W?
"void"
W?
")"
W?
";"
W?
"int"
W
"main"
W?
"("
W?
")"
W?
"{"
W?
POST = W? "return" W "0" W? ";" W? "}" W?
D = "int" W V W? ";"
V = [a-z,A-Z] [a-z,A-Z,0-9]*
I = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
NO = "+" | "-" | "*"
BO = "<" | ">" | "<=" | ">=" | "==" | "!="
BC = "&&" | "||" | "==" | "!="
W = (" " | "\n") (" " | "\n")*
}}}

Calls to {{{__VERIFIER_nondet_int()}}} yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.

C Integer Programs

2015-06-22T12:57:42Z

Cryingshadow: Add new page for integer C category

[[Category:Categories]]

Non-terminals:
P: Program
PRE: Start of the program, including the declaration of an external
function for non-deterministic values
POST: The end of the program
D: Variable declaration
V: Variable name
INS: Instruction
A: Assignment
L: Loop
C: Condition
NE: Numerical expression
N: Number
BE: Boolean expression
NO: Numerical operator
BO: Boolean operator
BC: Boolean connective
W: Whitespace

Grammar:
P = PRE D* W? I* POST
PRE = W?
"extern"
W
"int"
W
"__VERIFIER_nondet_int"
W?
"("
W?
"void"
W?
")"
W?
";"
W?
"int"
W
"main"
W?
"("
W?
")"
W?
"{"
W?
POST = W? "return" W "0" W? ";" W? "}" W?
D = "int" W V W? ";"
V = [a-z,A-Z] [a-z,A-Z,0-9]*
I = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* W? "}")?
NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
NO = "+" | "-" | "*"
BO = "<" | ">" | "<=" | ">=" | "==" | "!="
BC = "&&" | "||" | "==" | "!="
W = (" " | "\n") (" " | "\n")*

Calls to __VERIFIER_nondet_int() yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.

Termination Competition

2015-06-22T12:44:30Z

Cryingshadow: Update upcoming competition

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007, the competition organizer was Claude Marche, [http://www.lri.fr/~marche/termination-competition/ Paris].
Since 2008 the competition was run by Rene Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
For 2014, we intend to move to the [https://www.starexec.org/ Star Exec] platform (at U Iowa).

== Upcoming Competitions ==

The [[Termination_Competition_2015|Termination Competition 2015]] will be affiliated with [http://conference.mi.fu-berlin.de/cade-25/home CADE].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
Extensions under consideration for 2014
* [[C Programs]]
* [[Transition Systems]]
Longer term plans
* [[ITRS|integer term rewriting]]

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2014]], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/20 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]
* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Termination Competition 2014 Questionnaire

2014-08-02T12:52:33Z

Cryingshadow:

The following questions regarding Star-Exec are being asked by Aaron Stump and Cesare Tinelli,
to all Summer 2014 competition organizers. I (J.W.) will answer, by August 5, and I'd like to collect your comments here.
Just enter below the question, but keep the question intact. (I am dropping some administrative questions, but keep the original numbering.)

== 4. What were the advantages and disadvantages of using StarExec for you as competition organizer, in comparison with whatever alternative you would have utilized instead of StarExec? ==

== 5. What were the most positive aspects of your experience running your competition on StarExec? ==

It is not longer necessary to maintain hardware and software for each competition separately. This makes the competition more independent of individual research groups and their funding.

The computing power allowed us to run the competition in much less time than before.

== 6. What were the negative aspects? ==

It was not (easily) possible to install auxiliary software needed by the tools.

It was not possible to access remote machines from StarExec, which is needed for some commercial tools that are not willing to let their binaries run on StarExec itself.

Restrictions (e.g., on the name length) for benchmarks prevented the submission of whole benchmark sets instead of just those files violating the restrictions. Only one error was displayed at a time and the user had to successively remove files from the benchmark set before the submission succeeded.

The allowed characters for tool descriptions were very restricted and did not allow a nice representation, e.g., of author names containing special characters. In particular, the restrictions were not documented in a way that the user would know about the restrictions beforehand, but needed to try out several versions until a description was accepted.

== 10. Where do you think we should focus our development efforts going forward? ==
A few of the things we are considering are: additional interfaces for viewing job results (maybe similar to the 2-dimensional grid used in Termination; other suggestions?), solver pipelines (output from one stage becomes benchmark for input to the next stage; other details to be determined), more work to make it possible to install and run StarExec on your own server or computer (abstract out security-critical details, installation documention, and abstract the interface to GridEngine so you can use a different third-party tool to run jobs on a cluster, or even just your own desktop), commitment to and documentation of the URLs used for communicating directly with the server. Documentation of restrictions and registration procedures.

== 11. Do you expect you or your colleagues will likely want to run the next edition of your competition on StarExec? ==

== 12. How adequate was the help you were able to get either directly from the StarExec team or from the forum? ==

Response times could easily exceed one or in some cases even several weeks.

== 13. How satisfied do you perceive the participants in your competition were with their experience using StarExec? ==

The submission phase felt very chaotic and submissions involved much more work for the participants than in previous years. The execution phase seemed to run smoothly (at least from the participants' perspective) and very fast.

== 14. Were there any recurring issues or complaints from the participants in your competition? ==

See answers to question 6.

== 15. Any further comments or suggestions? ==

C Programs

2014-07-02T11:13:12Z

Cryingshadow:

Termination Competition 2014

2014-06-10T11:10:05Z

Cryingshadow: /* Registration Info (tentative) */

In 2014, the Termination Competition will be part of the [http://vsl2014.at/olympics/ FLoC Olympic Games].

== Dates (tentative) ==

* call for tools, certifiers, problems: May 26
* registration of tools: June 15
* updates of registered tools, submission of problems: July 1
* competition runs: July 15 - 20
* results announced: July 21, during the Second FLoC Olympic Games Award Ceremony, Vienna.

== Competition Categories and Awards ==

The competition contains several categories, grouped in three meta-categories:

* termination of term rewriting (all categories with HO/FO-TRSs, with- or without strategies)
* complexity analysis of term rewriting (all complexity categories)
* termination of programming languages (Logic Programming, Haskell, Java, C, ...)

In each meta-category, a medal will be awarded to the highest-scoring solver.

For every meta-category, we consider the sum of the scores for each category within that meta-category:
The score of a tool is determined by the number of other tools which could be beaten in that category.

This puts the emphasis on categories with many competitors.
(In particular, a category with just one entrant would produce a zero score.)
A category is only run at the competition if there are at least 2 participants and at least 40 examples
for this category in the underlying termination problem data base.

== New Categories ==

This year a new category on termination of C programs will be included (see the details [http://www.termination-portal.org/wiki/C_Programs here]).

Other categories for "transition systems" or "large scale (Java) programs" are under consideration depending on the number of interested participants and available problems.

== Competition Procedure ==

All participants in the same category will be run on a [http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm subset] of the existing problems of this category. The number of problems used in the competition is not fixed and will depend on the number of existing problems. The problem selection algorithm will be the same as in previous years (link http://www.termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm), however because of moving to [http://www.starexec.org StarExec], there might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 60 (up to 300) seconds, and 4 cores will be available (if a tool wants to use concurrent execution).

For nearly all categories, the tools will be started in their directory and obtain two parameters:

* the problem file and
* the timeout in seconds.

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized with a high negative score. Moreover, those buggy systems may have the opportunity to provide a corrected version that will be run again after the end of the live execution (displaying the new results afterwards, but out of competition).

For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non-contradictory answers minus the given penalization (if any).

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Frederic Mesnard, Université de la Réunion, France
* Albert Rubio (chair), UPC Barcelona, Spain
* Rene Thiemann, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany
* Stefan von der Krone, HTWK Leipzig, Germany

== Registration Info (tentative) ==

Participants must register on [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec].

Note: if I (J. Waldmann) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader). The email address you give in the registration should be your institutional one.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== Technical Detail ==

We intend to run the competition on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Technical details about the execution platform can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de.

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Logic Programming

2012-05-23T09:16:05Z

Cryingshadow: /* Syntax/Semantics for Input/Output */ adapted to current competition customs

This page is to record the current status of discussion
on cleaning up the Logic Programming Category of the Termination Competition.

(Discussion should take place on the termtools mailing list.)

== Syntax/Semantics for Input/Output ==

The set of queries, for which termination should be analyzed, is
given by a comment of the form "%query: <predicate>(<arguments>).".
Here, <predicate> is the root symbol of all queries to analyze
while <arguments> is a comma-separated list of argument indicators
which specify whether the argument at the particular position must
be a ground term or can be an arbitrary term. There are three pairs
of argument indicators in use (historically grown) where the first
indicator specifies ground arguments and the second specifies
arbitrary arguments: i and o (for input and output), b and f (for
bound and free), and g and a (for ground and any).
Example:

%query: p(i,o).

This means all queries :- p(s,t). where s is a ground term
and t can be any term.
If the root symbol has no arguments, the parantheses are omitted.
Example:

%query: p.

== Problematic Examples ==

The following examples are empty:
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/gt_mod.pl

The following examples contain non-trivial built-in predicates that are potentially
handled in very different ways by the individual tools (leading to potentially
different termination status):
* LP/lpexamples/factorial.pl
* LP/lpexamples/fib-oi.pl
* LP/lpexamples/fib.pl
* LP/lpexamples/hanoi.pl
* LP/lpexamples/kay4.pl
* LP/lpexamples/numbervars.pl
* LP/lpexamples/primes.pl
* LP/lpexamples/tautology.pl
* LP/lpexamples/totient.pl
* LP/talp/apt/curry_ap.pl
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/dc_schema.pl
* LP/talp/apt/gt_mod.pl
* LP/talp/apt/gtsolve.pl
* LP/talp/apt/mergesort_ap_variant.pl
* LP/talp/maria/aiakl.pl
* LP/talp/maria/ann.pl
* LP/talp/maria/bid.pl
* LP/talp/maria/boyer.pl
* LP/talp/maria/browse.pl
* LP/talp/maria/deriv-oii.pl
* LP/talp/maria/deriv.pl
* LP/talp/maria/fib.pl
* LP/talp/maria/grammar.pl
* LP/talp/maria/grammar2.pl
* LP/talp/maria/hanoiapp.pl
* LP/talp/maria/mmatrix.pl
* LP/talp/maria/money.pl
* LP/talp/maria/occur.pl
* LP/talp/maria/peephole.pl
* LP/talp/maria/progeom.pl
* LP/talp/maria/qplan.pl
* LP/talp/maria/qsortapp.pl
* LP/talp/maria/query.pl
* LP/talp/maria/rdtok.pl
* LP/talp/maria/read.pl
* LP/talp/maria/serialize.pl
* LP/talp/maria/tak.pl
* LP/talp/maria/tictactoe.pl
* LP/talp/maria/warplan.pl
* LP/talp/taboch/permute2.pl
* LP/talp/taboch/queens.pl
* LP/terminweb/old-terminweb/mergesort.pl
* LP/terminweb/old-terminweb/queens.pl
* LP/terminweb/old-terminweb/quicksort.pl

== Questions ==

* should empty examples be removed?
* how to handle built-ins that the tool does not support?
* do we want to have a (sub-)category "pure logic programs"?

== Unification with or without Occurs Check ==

Currently, there are some examples in the LP-Prolog category where
termination depends on whether unification is performed with or
without the occurs check. Following the treatment of overflows in
the Java categories, in such cases both YES and NO answers (with
consistent proofs) are valid.

== Participants ==

The following is a list of participants to this category
* [[Tools:AProVE]]

[[Category:Categories]]

Logic Programming

2011-05-24T09:25:56Z

Cryingshadow:

This page is to record the current status of discussion
on cleaning up the Logic Programming Category of the Termination Competition.

(Discussion should take place on the termtools mailing list.)

== Syntax/Semantics for Input/Output ==

The set of queries, for which termination should be analyzed, is
given by a comment in the first line. Example:

%query: p(i,o).

This means all queries :- p(s,t). where s is a ground term
and t can be any term.

== Problematic Examples ==

The following examples are empty:
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/gt_mod.pl

The following examples contain non-trivial built-in predicates that are potentially
handled in very different ways by the individual tools (leading to potentially
different termination status):
* LP/lpexamples/factorial.pl
* LP/lpexamples/fib-oi.pl
* LP/lpexamples/fib.pl
* LP/lpexamples/hanoi.pl
* LP/lpexamples/kay4.pl
* LP/lpexamples/numbervars.pl
* LP/lpexamples/primes.pl
* LP/lpexamples/tautology.pl
* LP/lpexamples/totient.pl
* LP/talp/apt/curry_ap.pl
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/dc_schema.pl
* LP/talp/apt/gt_mod.pl
* LP/talp/apt/gtsolve.pl
* LP/talp/apt/mergesort_ap_variant.pl
* LP/talp/maria/aiakl.pl
* LP/talp/maria/ann.pl
* LP/talp/maria/bid.pl
* LP/talp/maria/boyer.pl
* LP/talp/maria/browse.pl
* LP/talp/maria/deriv-oii.pl
* LP/talp/maria/deriv.pl
* LP/talp/maria/fib.pl
* LP/talp/maria/grammar.pl
* LP/talp/maria/grammar2.pl
* LP/talp/maria/hanoiapp.pl
* LP/talp/maria/mmatrix.pl
* LP/talp/maria/money.pl
* LP/talp/maria/occur.pl
* LP/talp/maria/peephole.pl
* LP/talp/maria/progeom.pl
* LP/talp/maria/qplan.pl
* LP/talp/maria/qsortapp.pl
* LP/talp/maria/query.pl
* LP/talp/maria/rdtok.pl
* LP/talp/maria/read.pl
* LP/talp/maria/serialize.pl
* LP/talp/maria/tak.pl
* LP/talp/maria/tictactoe.pl
* LP/talp/maria/warplan.pl
* LP/talp/taboch/permute2.pl
* LP/talp/taboch/queens.pl
* LP/terminweb/old-terminweb/mergesort.pl
* LP/terminweb/old-terminweb/queens.pl
* LP/terminweb/old-terminweb/quicksort.pl

== Questions ==

* should empty examples be removed?
* how to handle built-ins that the tool does not support?
* do we want to have a (sub-)category "pure logic programs"?

== Unification with or without Occurs Check ==

Currently, there are some examples in the LP-Prolog category where
termination depends on whether unification is performed with or
without the occurs check. Following the treatment of overflows in
the Java categories, in such cases both YES and NO answers (with
consistent proofs) are valid.

== Participants ==

The following is a list of participants to this category
* [[Tools:AProVE]]

[[Category:Categories]]

Logic Programming

2011-05-24T09:20:28Z

Cryingshadow:

This page is to record the current status of discussion
on cleaning up the Logic Programming Category of the Termination Competition.

(Discussion should take place on the termtools mailing list.)

== Syntax/Semantics for Input/Output ==

The set of queries, for which termination should be analyzed, is
given by a comment in the first line. Example:

%query: p(i,o).

This means all queries :- p(s,t). where s is a ground term
and t can be any term.

== Problematic Examples ==

The following examples are empty:
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/gt_mod.pl

The following examples contain non-trivial built-in predicates that are potentially
handled in very different ways by the individual tools (leading to potentially
different termination status):
* LP/lpexamples/factorial.pl
* LP/lpexamples/fib-oi.pl
* LP/lpexamples/fib.pl
* LP/lpexamples/hanoi.pl
* LP/lpexamples/kay4.pl
* LP/lpexamples/numbervars.pl
* LP/lpexamples/primes.pl
* LP/lpexamples/tautology.pl
* LP/lpexamples/totient.pl
* LP/talp/apt/curry_ap.pl
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/dc_schema.pl
* LP/talp/apt/gt_mod.pl
* LP/talp/apt/gtsolve.pl
* LP/talp/apt/mergesort_ap_variant.pl
* LP/talp/maria/aiakl.pl
* LP/talp/maria/ann.pl
* LP/talp/maria/bid.pl
* LP/talp/maria/boyer.pl
* LP/talp/maria/browse.pl
* LP/talp/maria/deriv-oii.pl
* LP/talp/maria/deriv.pl
* LP/talp/maria/fib.pl
* LP/talp/maria/grammar.pl
* LP/talp/maria/grammar2.pl
* LP/talp/maria/hanoiapp.pl
* LP/talp/maria/mmatrix.pl
* LP/talp/maria/money.pl
* LP/talp/maria/occur.pl
* LP/talp/maria/peephole.pl
* LP/talp/maria/progeom.pl
* LP/talp/maria/qplan.pl
* LP/talp/maria/qsortapp.pl
* LP/talp/maria/query.pl
* LP/talp/maria/rdtok.pl
* LP/talp/maria/read.pl
* LP/talp/maria/serialize.pl
* LP/talp/maria/tak.pl
* LP/talp/maria/tictactoe.pl
* LP/talp/maria/warplan.pl
* LP/talp/taboch/permute2.pl
* LP/talp/taboch/queens.pl
* LP/terminweb/old-terminweb/mergesort.pl
* LP/terminweb/old-terminweb/queens.pl
* LP/terminweb/old-terminweb/quicksort.pl

== Questions ==

* should empty examples be removed?
* how to handle built-ins that the tool does not support?
* do we want to have a (sub-)category "pure logic programs"?

== Unification with or without Occurs-Check ==

Currently, there are some examples in the LP-Prolog category where
termination depends on whether unification is performed with or
without the occurs-check. Following the treatment of overflows in
the Java categories, in such cases both YES and NO answers (with
consistent proofs) are valid.

== Participants ==

The following is a list of participants to this category
* [[Tools:AProVE]]

[[Category:Categories]]