Treffer: Bounded satisfiability checking of FOL∗ formulas with aggregations.

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. [ABSTRACT FROM AUTHOR]

Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)