Concept

Lindström quantifier

Publications associées (53)

Counterexample-Guided Focus

The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right ...

2010

Stochastic Optimization of Sailing Trajectories in an America's Cup Race

Frédéric Dumas

The main objective of the thesis is the study and the determination of an optimal navigation strategy, for a sailboat in an America's Cup race, by methods of stochastic optimization. Such methods are appropriate because the sailing team expects the wind to ...

EPFL2010

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

Modelling the influence of human behaviour on the spread of infectious diseases: a review

Marcel Salathé

Human behaviour plays an important role in the spread of infectious diseases, and understanding the influence of behaviour on the spread of diseases can be key to improving control efforts. While behavioural responses to the spread of a disease have often ...

2010

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

On Large Deviation Regimes For Random Media Models

Thomas Mountford, Damien Gauthier, Michael Cranston

The focus of this article is on the different behavior of large deviations of random subadditive functionals above the mean versus large deviations below the mean in two random media models. We consider the point-to-point first passage percolation time a(n ...

2009

Omnidirectional Pulse Dispersion of Planar Circular Monopoles

Anja Skrivervik, Gabriela Quintero Diaz De Leon

Three antenna systems, composed of circular monopoles with different ground plane sizes, are studied. The transmission of an UWB pulse between two identical monopoles is analyzed. The omnidirectional properties of the UWB antennas are measured and simulate ...

IEEE Service Center, 445 Hoes Lane, Po Box 1331, Piscataway, Nj 08855-1331 Usa2009

Quench propagation in coated conductors for fault current limiters

Frédéric Sirois, François Roy, Bertrand Dutoit

A fundamental understanding of the quench phenomenon is crucial in the future design and operation of high temperature superconductors based fault current limiters. The key parameter that quantifies the quenching process in superconductors is the normal zo ...

2009

RedOx study of anode supported solid oxide fuel cell

Jan Van Herle, Aïcha Hessler-Wyser, Antonin Faes, Arata Nakajo, David Dubois

The common technology for solid oxide fuel cells (SOFC) is based on a cermet (ceramic-metal composite) anode of nickel with yttria stabilized zirconia (YSZ), often used as the supporting structure. One of the main limitations of this technology is the tole ...

2009

Non-Clausal Satisfiability Modulo Theories

Philippe Paul Henri Suter

This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is resp ...

2008

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