Combined Reasoning with Sets and Aggregation Functions
Author: Markus Bender
Paper Information
| Title: | Combined Reasoning with Sets and Aggregation Functions |
| Authors: | Markus Bender |
| Proceedings: | ARW-DT 2014 - Automated Reasoning Workshop/Deduktionstreffen Proceedings |
| Editor: | Manfred Kerber |
| Keywords: | Satisfiability Modulo Theories, Boolean Algebra and Presburger Arithmetic, Program Verification |
| Abstract: | ABSTRACT. We developed a method that allows to check the satisfiability 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 task lie in this fragment, this method can be used for checking the behaviour of a program. |
| Pages: | 0 |
| Talk: | Jul 23 17:00 |
| Paper: |  |