ML p(r)ior | Counting Constraints in Flat Array Fragments

Counting Constraints in Flat Array Fragments

2016-02-01
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.
PDF

Highlights - Most important sentences from the article

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

Related Articles

2019-05-19

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

Highlights - Most important sentences from the article

2019-05-14
1905.05665 | cs.LO

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

Highlights - Most important sentences from the article

2017-04-12

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

Highlights - Most important sentences from the article

2019-03-06
1903.02344 | cs.LO

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

Highlights - Most important sentences from the article

2018-10-25
1810.10899 | cs.LO

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

Highlights - Most important sentences from the article

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
PDF

Highlights - Most important sentences from the article

2017-03-01

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

Highlights - Most important sentences from the article

2018-10-31

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

Highlights - Most important sentences from the article

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
PDF

Highlights - Most important sentences from the article

2018-05-25
1805.10073 | cs.LO

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

Highlights - Most important sentences from the article

2018-09-13
1809.04772 | cs.LO

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

Highlights - Most important sentences from the article

2017-12-19
1712.06868 | cs.LO

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

Highlights - Most important sentences from the article

2014-05-13

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

Highlights - Most important sentences from the article

2016-07-07

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

Highlights - Most important sentences from the article

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
PDF

Highlights - Most important sentences from the article

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
PDF

Highlights - Most important sentences from the article

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