Maximilian Jaroschek

Date: 10:30, Tuesday, May 2, 2017
Speaker: Maximilian Jaroschek
Venue: TU Wien

EI 4 Reithoffer HS, Gußhausstraße 25, 10:30


Analyzing and reasoning about safety properties of software systems
becomes an especially challenging task for programs with complex flow
and, in particular, with loops or recursion. For such programs one needs
additional information, for example in the form of loop invariants,
expressing properties to hold at intermediate program points. We study
program loops with non-trivial arithmetic, implementing addition and
multiplication among numeric program variables. In this talk, we present
a new approach for automatically generating all polynomial invariants of
a class of such programs, based on techniques from computer algebra,
which will be explained thoroughly and intuitively.

Posted in RiSE Seminar