Concept

Satisfiability modulo theories

Publications associées (73)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

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

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

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

MUNCH - Automated Reasoner for Sets and Multisets

Viktor Kuncak, Ruzica Piskac

This system description provides an overview of the MUNCH reasoner for sets and multisets. MUNCH takes as the input a formula in a logic that supports expressions about sets, multisets, and integers. Constraints over collections and integers are connected ...

Springer2010

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

Algebraic, AIDA/Cube and Side Channel Analysis of KATAN Family of Block Ciphers

Pouyan Sepehrdad, Jorge Nakahara

This paper presents the first results on AIDA/cube, algebraic and side-channel attacks on variable number of rounds of all members of the KATAN family of block ciphers. Our cube attacks reach 60, 40 and 30 rounds of KATAN32, KATAN48 and KATAN64, respective ...

Springer2010

Proving memory safety of floating-point computations by combining static and dynamic program analysis

Johannes Kinder

Whitebox fuzzing is a novel form of security testing based on dynamic symbolic execution and constraint solving. Over the last couple of years, whitebox fuzzers have found many new security vulnerabilities (buffer overflows) in Windows and Linux applicatio ...

ACM Press2010

Complete Program Synthesis for Linear Arithmetic

Mikaël Mayer

Synthesis of programs or their fragments is a way to write programs by providing only their meaning without worrying about the implementation details. It avoids the drawback of writing sequential code, which might be difficult to check, error-prone or tedi ...

2010

Enhancing numerical constraint propagation using multiple inclusion representations

Boi Faltings, Xuan-Ha Vu

Building tight and conservative enclosures of the solution set is of crucial importance in the design of efficient complete solvers for numerical constraint satisfaction problems (NCSPs). This paper proposes a novel generic algorithm enabling the cooperati ...

Springer Netherlands2009

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