Concept

Formule logique

Publications associées (49)

The Entropy of Conditional Markov Trajectories

Patrick Thiran, Matthias Grossglauser, Mohamed Kafsi

To quantify the randomness of Markov trajectories with fixed initial and final states, Ekroot and Cover proposed a closed-form expression for the entropy of trajectories of an irreducible finite state Markov chain. Numerous applications, including the stud ...

2013

Analytical approximations for the collapse of an empty spherical bubble

Mohamed Farhat, Danail Obreschkow

The Rayleigh equation 3/2 (R) over dot + R(R) double over dot + p rho(-1) = 0 with initial conditions R(0) = R-0, (R) over dot(0) = 0 models the collapse of an empty spherical bubble of radius R(T) in an ideal, infinite liquid with far-field pressure p and ...

2012

Spatially coupled ensembles universally achieve capacity under belief propagation

Rüdiger Urbanke, Shrinivas Kudekar

We investigate spatially coupled code ensembles. For transmission over the binary erasure channel, it was recently shown that spatial coupling increases the belief propagation threshold of the ensemble to essentially the maximum a-priori threshold of the u ...

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

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

EPFL2011

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

On the accuracy of approximate techniques for the evaluation of lightning electromagnetic fields along a mixed propagation path

Marcos Rubinstein, Abdolhamid Shoory, Abdenabi Mimouni

In this paper we review simplified analytical expressions derived by Wait using the concept of attenuation function for the analysis of the propagation of lightning-radiated electromagnetic fields over a mixed propagation path (vertically stratified ground ...

2011

On Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

2010

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

Modeling complex intersections with the cell-transmission model

Gunnar Flötteröd

This article widens the scope of the cell-transmission model (CTM) to the modeling of urban traffic, which is dominated by intersection dynamics. The CTM has originally been proposed for freeways, and it is not immediately applicable to urban traffic for t ...

2009

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