2021/02/10 by Maximiliano Cristiá, Cristiá, Maximiliano, Gianfranco Rossi +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2102.05422
openalex publication_date 2021/02/10 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Formal reasoning about finite sets and cardinality is an important tool for\nmany applications, including software verification, where very often one needs\nto reason about the size of a given data structure and not only about what its\nelements are. The Constraint Logic Programming tool log provides a decision\nprocedure for deciding the satisfiability of formulas involving very general\nforms of finite sets, without cardinality. In this paper we adapt and integrate\na decision procedure for a theory of finite sets with cardinality into log.\nThe proposed solver is proved to be a decision procedure for its formulas.\nBesides, the new CLP instance is implemented as part of the log tool. In\nturn, the implementation uses Howe and King's Prolog SAT solver and Prolog's\nCLP(Q) library, as an integer linear programming solver. The empirical\nevaluation of this implementation based on +250 real verification conditions\nshows that it can be useful in practice.\n