Publication

Decision Procedures for Program Synthesis and Verification

Related publications (95)

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.

Collections, Cardinalities, and Relations

Viktor Kuncak, Ruzica Piskac

Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to co ...

2010

Strategy logic

We introduce strategy logic, a logic that treats strategies in two-player games as explicit first-order objects. The explicit treatment of strategies allows us to specify properties of nonzero-sum games in a simple and natural way. We show that the one-alt ...

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 ...

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

On Decision Procedures for Ordered Collections

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

We describe a decision procedure for a logic that supports 1) finite collections of elements (sets or multisets), 2) the cardinality operator, 3) a total order relation on elements, and 4) min and max operators on entire collections. Among the applications ...

2010

In defense of large qualitative calculi

Jingshi Li

The next challenge in qualitative spatial and temporal reasoning is to develop calculi that deal with different aspects of space and time. One approach to achieve this is to combine existing calculi that cover the different aspects. This, however, can lead ...

2010

Optimization of operations in container terminals: hierarchical vs integrated approaches

Michel Bierlaire, Matteo Salani, Ilaria Vacca

Over the last years, international sea freight container transportation has grown dramatically and container terminals play nowadays a key role within the global shipping network. Terminal's operations have received increasing interest in the scientific li ...

2010

Optimization in container terminals: hierarchical vs integrated solution approaches

Michel Bierlaire, Matteo Salani, Ilaria Vacca

Over the last years, international sea freight container transportation has grown dramatically and container terminals play nowadays a key role within the global shipping network. Terminals operations have received increasing interest in the scientific lit ...

2010

On inconsistent entities. A reply to Colyvan

Francesco Piazza

In a recent article M. Colyvan has argued that Quinean forms of scientific realism are faced with an unexpected upshot. Realism concerning a given class of entities, along with this route to realism, can be vindicated by running an indispensability argumen ...

2010

On Locality of One-Variable Axioms and Piecewise Combinations

Viktor Kuncak, Swen Jacobs

Local theory extensions provide a complete and efficient way for reasoning about satisfiability of certain kinds of universally quantified formulas modulo a background theory. They are therefore useful in automated reasoning, software verification, and syn ...

2010

Automatic Verification of Parametric Specifications with Complex Topologies

Swen Jacobs

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple ve ...

2010