### Counting Constraints in Flat Array Fragments

**2016-02-01**

1602.00458 | cs.LO

We identify a fragment of Presburger arithmetic enriched with free function
symbols and cardinality constraints for interpreted sets, which is amenable to
automated analysis. We establish decidability and complexity results for such a
fragment and we implement our algorithms. The experiments run in discharging
proof obligations coming from invariant checking and bounded model-checking
benchmarks show the practical feasibility of our decision procedure.

**Login to like/save this paper, take notes and configure your recommendations**

# Related Articles

**2019-05-19**

1905.07805 | cs.PL

Verification of fault-tolerant distributed protocols is an immensely
difficult task. Often, in these… show more

**2019-05-14**

1905.05665 | cs.LO

In this paper we show several similarities among logic systems that deal
simultaneously with deducti… show more

**2017-04-12**

1704.03772 | cs.LO

For a regular cardinal $\kappa$, a formula of the modal $\mu$-calculus is
$\kappa$-continuous in a v… show more

**2019-03-06**

1903.02344 | cs.LO

Propositional team logic is the propositional analog to first-order team
logic. Non-classical atoms … show more

**2018-10-25**

1810.10899 | cs.LO

We consider the one-variable fragment of first-order logic extended with
Presburger constraints. The… show more

**2019-03-30**

1904.00189 | cs.LO

We show that over the class of linear orders with additional binary relations
satisfying some monoto… show more

**2017-03-01**

1703.00544 | cs.CC

This paper settles the computational complexity of model checking of several
extensions of the monad… show more

**2018-10-31**

1810.13129 | cs.LO

This paper presents a new technique for optimizing formal analysis of
propositional logic formulas a… show more

**2018-10-22**

1810.09142 | cs.LO

We show that Branching-time temporal logics CTL and CTL*, as well as
Alternating-time temporal logic… show more

**2018-05-25**

1805.10073 | cs.LO

We propose an automated method for computing inductive invariants applied to
check deadlock-freedom … show more

**2018-09-13**

1809.04772 | cs.LO

We present a recursive formulation of the Horn algorithm for deciding the
satisfiability of proposit… show more

**2017-12-19**

1712.06868 | cs.LO

For relational monadic formulas (the L\"owenheim class) second-order
quantifier elimination, which i… show more

**2014-05-13**

1405.3250 | cs.AI

In this paper we study lifted inference for the Weighted First-Order Model
Counting problem (WFOMC),… show more

**2016-07-07**

1607.01993 | cs.LO

We investigate array separation logic (ASL), a variant of symbolic-heap
separation logic in which th… show more

**2012-01-23**

1201.4856 | cs.LO

In a recently launched research program for developing logic as a formal
theory of (interactive) com… show more

**2017-07-19**

1707.05945 | cs.LO

We study an extension of first-order logic that allows to express cardinality
conditions in a simila… show more

**2014-01-15**

1401.3475 | cs.LO

Prime implicates and prime implicants have proven relevant to a number of
areas of artificial intell… show more