Bounded Satisfiability Checking of FOL * Formulas with Aggregations

Abstract Software systems handling data are increasingly required to comply with legal properties (LPs) aimed at ensuring security and data privacy. Automated reasoning of LPs can be carried out by solving constraint satisfiability problems in first-order logic. However, the current logic-based reasoning approaches have limited support for capturing and reasoning about LPs with aggregation constraints, which are commonly found in financial and privacy policies. In this work, we extend first-order logic with quantifiers over relational objects (FOL *) to support aggregation, resulting in a language FOL * + , and propose a satisfiability checking algorithm, LEGOS-A, for FOL * + which supports reasoning about aggregation by over-and under-approximating the aggregated values and incrementally refining these approximations to derive the satisfiability result. Running LEGOS-A on real world and academic examples with aggregation from various domains showed that LEGOS-A was able to solve many previously intractable problems and provided substantial speed-ups compared to the state-of-the-art FOL * satisfiability checker and other SMT-based alternatives.