Concept

Prover9

Publications associées (32)

Spiral spin-liquid and the emergence of a vortex-like state in MnSc2S4

Jonathan White, Gregory Scott Tucker, Romain Sibille, Shang Gao

Spirals and helices are common motifs of long-range order in magnetic solids, and they may also be organized into more complex emergent structures such as magnetic skyrmions and vortices. A new type of spiral state, the spiral spin-liquid, in which spins f ...

Nature Publishing Group2017

Non-autonomous functionals, borderline cases and related function classes

Maria Colombo

The class of non-autonomous functionals under study is characterized by the fact that the energy density changes its ellipticity and growth properties according to the point; some regularity results are proved for related minimizers. These results are the ...

2016

Method and device for proving his identity

Serge Vaudenay, Ioana Cristina Carlson

The invention is related to a method allowing a prover holding a secret key (x) to prove its identity to a verifier and to prove to this verifier that he is within a predetermined distance of this verifier, said method comprising an initialization phase du ...

2015

Indoor Scene Recognition using Task and Saliency-driven Feature Pooling

Barbara Caputo, Marco Fornoni

Indoor scenes are characterized by a high intra-class variability, mainly due to the intrinsic variety of the objects in them, and to the drastic image variations due to (even small) view-point changes. One of the main trends in the literature has been to ...

2012

Real time multi-object tracking using multiple cameras

Michail Zervos

We build a real-time multi-people tracker, which is based on the Kalman Filter. The input to the software is a Probabilistic Occupancy Map of the observed area. The main goal of the project is to incorporate this tracker to the real-time detection software ...

2012

Sequential Topic Models for Mining Recurrent Activities and their Relationships

Jagannadan Varadarajan

In this thesis, we address the analysis of activities from long term data logs with an emphasis on video recordings. Starting from simple words from video, we progressively build methods to infer higher level scene semantics. The main strategies used to ac ...

EPFL2012

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

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

Systematic Evaluation Methodology and Performance Metrics for Haptic Interfaces

Evren Samur

The purpose of evaluation procedures for haptic interfaces is to achieve both qualitative and quantitative statements on haptic rendering realism and performance. Since haptics technology is being increasingly used in computer games, surgical simulators, m ...

EPFL2010

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

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