MOVES Seminar 4 May 2010
Andreas Kelle-Emden
Parallelizing automated termination analysis
Abstract:
Parallelized software is more and more important as modern CPUs reach
the physical limits of computation speed. Nowadays, most of the CPUs,
even for home computers, have at least two cores. Using more then one
core concurrently in an efficient way is very challenging because of
several side effects.
Automated termination analysis is also an important topic. As the
complexity of software systems grows dramatically, it is nearly
impossible to get an overview of their functionalities. This gives
rise to the need of reliable correctness proofs. Termination is
thereby an essential factor.
This thesis is the attempt to bring together both topics. I discuss
several ways to optimize the concurrency behaviour of our
state-of-the-art termination analyzer AProVE. Beginning with the
environment, in which AProVE runs, and then going further into the
details, I make AProVE run more efficiently on multicore machines,
thus being more powerful than before.
Abstract:
Parallelized software is more and more important as modern CPUs reach
the physical limits of computation speed. Nowadays, most of the CPUs,
even for home computers, have at least two cores. Using more then one
core concurrently in an efficient way is very challenging because of
several side effects.
Automated termination analysis is also an important topic. As the
complexity of software systems grows dramatically, it is nearly
impossible to get an overview of their functionalities. This gives
rise to the need of reliable correctness proofs. Termination is
thereby an essential factor.
This thesis is the attempt to bring together both topics. I discuss
several ways to optimize the concurrency behaviour of our
state-of-the-art termination analyzer AProVE. Beginning with the
environment, in which AProVE runs, and then going further into the
details, I make AProVE run more efficiently on multicore machines,
thus being more powerful than before.
