Publication

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Related publications (47)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Decision Procedures for Automating Termination Proofs

Ruzica Piskac

Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current too ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

On Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

2010

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

On Deciding Functional Lists with Sublist Sets

Viktor Kuncak

Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for lo ...

2010

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2010

Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...

Springer2009

On Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...

2009

On Set-Driven Combination of Logics and Verifiers

Viktor Kuncak

We explore the problem of automated reasoning about the non-disjoint combination of logics that share set variables and operations. We prove a general combination theorem, and apply it to show the decidability for the quantifier-free combination of formula ...

2009

Decision Procedures for Multisets with Cardinality Constraints

Viktor Kuncak, Ruzica Piskac

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...

Springer2008