Concept

Méthode formelle (informatique)

Publications associées (377)

Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric: Performance Guarantees and Tractable Reformulations

We consider stochastic programs where the distribution of the uncertain parameters is only observable through a finite training dataset. Using the Wasserstein metric, we construct a ball in the space of (multivariate and non-discrete) probability distribut ...

2018

Highly Active Nanoperovskite Catalysts for Oxygen Evolution Reaction: Insights into Activity and Stability of Ba0.5Sr0.5Co0.8Fe0.2O2+delta and PrBaCo2O5+delta

Nicola Marzari, Ivano Eligio Castelli, Xi Cheng

It is shown that producing PrBaCo2O5+delta and Ba0.5Sr0.5Co0.8Fe0.2O2+delta nanoparticle by a scalable synthesis method leads to high mass activities for the oxygen evolution reaction (OER) with outstanding improvements by 10x and 50x, respectively, compar ...

WILEY-V C H VERLAG GMBH2018

Secure Contactless Payment

Serge Vaudenay, Handan Kilinç Alper

A contactless payment lets a card holder execute payment without any interaction (e.g., entering PIN or signing) between the terminal and the card holder. Even though the security is the first priority in a payment system, the formal security model of cont ...

2018

Extending Safe C Support In Leon

Marco Adriano Antognini

As hardware designs get more robust and efficient, software can solve a wider range of challenges, each one more advanced than the previous one. The direct consequence is that software complexity grows continuously. Despite being used more frequently in de ...

2017

Robust Control Policies Given Formal Specifications in Uncertain Environments

Maryam Kamgarpour, Tony Alan Wood

We consider robust control synthesis for linear systems with complex specifications that are affected by uncertain disturbances. This letter is motivated by autonomous systems interacting with partially known, time-varying environments. Given a specificati ...

2017

Towards Proving Optimistic Multicore Schedulers

Willy Zwaenepoel, Baptiste Joseph Eustache Lepers

Operating systems have been shown to waste machine resources by leaving cores idle while work is ready to be scheduled. This results in suboptimal performance for user applications, and wasted power. Recent progress in formal verification methods have led ...

2017

Type Soundness Proofs with Definitional Interpreters

Tiark Rompf, Nada Amin

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

Assoc Computing Machinery2017

Algorithmic Verification of Component-based Systems

Qiang Wang

This dissertation discusses algorithmic verification techniques for concurrent component-based systems modeled in the Behavior-Interaction-Priority (BIP) framework with both bounded and unbounded concurrency. BIP is a component framework for mixed software ...

EPFL2017

From Timed Component-Based Systems to Time-Triggered Implementations: A Correct-by-Design Approach

In hard real-time embedded systems, design and specification methods and their associated tools must allow development of temporally deterministic systems to ensure their safety. To achieve this goal, we are specifically interested in methodologies based o ...

CEA LIST2017

metaSMT: focus on your application and not on solver integration

Mathias Soeken, Heinz Riener

Many applications from artificial intelligence and formal methods use decision procedures as their core solving engines. In this context, automated reasoning based on Satisfiability (SAT) or Satisfiability Modulo Theories (SMT) is very effective. For a giv ...

Springer Verlag2017

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