Concept

Computer-assisted proof

Publications associées (32)

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

Automated quality control in MR-based brain morphometry

Jean-Philippe Thiran, Tobias Kober, Tom Hilbert, Bénédicte Marie Maréchal, Delphine Ribes Lemay, Reto Meuli, Alexis Roche

Normal aging and a wide range of neurologic, inflammatory or psychiatric diseases lead to changes in the brain tissue over time. In the interest of diagnosis, prognosis and treatment monitoring, it is highly desirable to have robust tools that reliably mea ...

2012

Bifurcation Analysis at a Singular Soliton State in Fiber Couplers

Boris Buffoni

The system {-u '' + u = u(3) + lambda v, u(x)= u(-x) is an element of R, x is an element of R, -v '' + v = v(3) + lambda u, v(x) = v(-x) is an element of R, x is an element of R, describes pulses in nonlinear fiber couplers. It has the family (U1+lambda, - ...

Advanced Nonlinear Studies, Inc2012

Verification of Imperative Programs in Scala

Régis William Blanc

Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a ...

2012

Faster and Smoother - VSH Revisited

Juraj Sarinay

We reconsider the provably collision resistant Very Smooth Hash and propose a small change in the design aiming to improve both performance and security. While the original proofs of security based on hardness of factoring or discrete logarithms are preser ...

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

On Satisfiability Modulo Computable Functions

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

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...

2010

Automatic quality assessment in structural brain magnetic resonance imaging

Jean-Philippe Thiran, Reto Meuli

Quality assessment of MRI is of great importance to derive reliable diagnostic information. As automated quantitative image analysis is being increasingly used in routine, automated measures of quality are needed. Based on a single magnitude image, we prop ...

2009

Asymptotics and analytic modes for the wave equation in similarity coordinates

Roland Donninger

We consider the radial wave equation in similarity coordinates within the semigroup formalism. It is known that the generator of the semigroup exhibits a continuum of eigenvalues and embedded in this continuum there exists a discrete set of eigenvalues wit ...

Springer Verlag2009