Concept

Quantifier elimination

Related publications (22)

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

Decision Procedures for Power Structures

Rodrigo Raya

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

EPFL2023

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

Springer, Cham2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Experimental study of impulse waves generated by viscoplastic fluid

Zhenzhu Meng

Landslide-generated waves, also called impulse waves, occur as a result of the intrusion of landslides (such as rock falls, debris flows, and avalanches) into bodies of water (such as lakes, reservoirs, and seas). The objective of this thesis was to study ...

EPFL2020

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

2017

Tralopyril bioconcentration and effects on the gill proteome of the Mediterranean mussel Mytilus galloprovincialis

Julita Maria Stadnicka-Michalak, Kevin Thomas

Antifouling (AF) systems are used worldwide as one of the most cost-effective ways of protecting submerged structures against heavy biofouling. The emergence of environmentally friendly AF biocides requires knowledge on their environmental fate and toxicit ...

Elsevier Science Bv2016

Product Pricing in a Peer-to-Peer Economy

Thomas Alois Weber

The emergence of a collaborative economy has been driven by advances in information technology that allow consumers to borrow and rent goods among peers on a secondary sharing market. In a dynamic setting, consumers make intertemporal decisions about purch ...

2016

A Verification Toolkit for Numerical Transition Systems

Viktor Kuncak, Hossein Hojjat

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

2012

Software Synthesis Procedures

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succ ...

2012

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

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

A Minimal Exercise Extension for Models of the Glucoregulatory System

Denis Gillet, Grégory François, Alain Bock, Thierry Prud'Homme

For patients with type 1 diabetes mellitus, appropriate control of blood glucose concentrations is vital. Exercise is one of the disturbances that can affect these concentrations. Therefore, predictions in the presence of exercise are useful among others f ...

Elsevier2011

Comfusy: A Tool for Complete Functional Synthesis

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesi ...

Springer2010

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

Performance of Anidolic Daylighting Systems in tropical climates – Parametric studies for identification of main influencing factors

Jean-Louis Scartezzini, Friedrich Linhart, Stephen Wittkopf

Making daylight more available in buildings is highly desirable, not only for reasons of energy-efficiency, but also for improvement of occupants’ health and well-being. Core-daylighting, that is daylight provision in areas situated at considerable distanc ...

Elsevier2010

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

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

Laura Ildiko Kovacs

We present a new method for automatic generation of loop invariants for programs containing arrays. Unlike all previously known methods, our method allows one to generate first-order invariants containing alternations of quantifiers. The method is based on ...

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

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