Publication

Collections, Cardinalities, and Relations

Viktor Kuncak, Ruzica Piskac
2010
Conference Papers

Abstract

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 compute direct and inverse relation and function images. We establish decidability and complexity bounds for the extended logics.

Official source

Graph Chat

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

Chat with Graph Search

Orthologic with Axioms

Interpolation and Quantifiers in Ortholattices

Efficient Continual Finite-Sum Minimization