[Termtools] Termination Competition 2015: Proposal for new integer C category

Thomas Ströder stroeder at informatik.rwth-aachen.de
Mon Jun 22 15:46:34 CEST 2015


Dear Steering Committee,

I would like to propose a new category on termination analysis of C
programs restricted to a small subset of C only operating on integers
using 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.

I added a corresponding page to the termination portal wiki where the
exact syntax and semantics are described:
http://www.termination-portal.org/wiki/C_Integer_Programs

The tool AProVE would certainly participate in this new category. I also
talked to Matthias Heizmann from the tool Ultimate Automizer and he
would be interested in this new category, too.

Best regards,

  Thomas

-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150622/6e42a31b/attachment.sig>


More information about the Termtools mailing list