Vortrag vom 25.06.2014

Vortragender: Markus Bender

Titel: Combined Reasoning with Sets and Aggregation Functions


The combined theory of sets and cardinalities can be used to model some tasks in program verification. A method for checking validity of formulae in this theory is known.
To extend this approach, we developed a method that allows to check the validity of a formula in the combined theories of sets and the bridging functions card, sum, avg, min, max by using a prover for linear arithmetic. Since abstractions of certain verification tasks lie in this fragment, this method can be used in program verification.