Concept

Arithmétique de Presburger

Publications associées (37)

Method and apparatus for low complexity spectral analysis of bio-signals

David Atienza Alonso, Andreas Peter Burg, Srinivasan Murali, Georgios Karakonstantis, Aviinaash Sankaranarayanan

A method and device for reducing the computational complexity of a processing algorithm, of a discrete signal, in particular of the spectral estimation and analysis of bio-signals, with minimum or no quality loss, which comprises steps of (a) choosing a do ...

2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...

Springer-Verlag Berlin2015

Generalized Bombieri-Lagarias' Theorem And Generalized Li'S Criterion With Its Arithmetic Interpretation

We show that Li's criterion equivalent to the Riemann hypothesis, i.e., the statement that the sums k(n) = Sigma(rho)(1-(1-1/rho)(n)) over zeros of the Riemann xi-function and the derivatives lambda(n) equivalent to 1/(n-1)! d(n)/dz(n)(z(n-1) ln (xi(z)))ve ...

Springer Verlag2014

Functional synthesis for linear arithmetic and sets

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. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way—they should succeed for a well-defin ...

Springer Berlin Heidelberg2013

Tree Interpolation in Vampire

Régis William Blanc, Laura Ildiko Kovacs, Ashutosh Gupta

We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of ...

Springer Berlin Heidelberg2013

Efficient Arithmetic Logic Gates Using Double-Gate Silicon Nanowire FETs, invited paper

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

Silicon NanoWire (SiNW) based Field Effect Tran- sistors (FETs) are promising candidates to extend Moore’s law in the coming years. Recently, Double-Gate (DG) SiNWFETs have been demonstrated to allow on-line configurability of n -type and p -type device po ...

2013

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

On Synthesis for Unbounded Bit-vector Arithmetic

Viktor Kuncak, Andrej Spielmann

We propose to describe computations using QFPAbit, a language of quantifier-free linear arithmetic on unbounded integers with bitvector operations. Given a QFPAbit formula with input and output variables, we describe an algo- rithm that generates an effici ...

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

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