Publications associées à Validation of Visual Contracts for Services

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

Technology Mapping Using Multi-output Library Cells

Giovanni De Micheli, Alessandro Tempia Calvino

Technology mapping transforms a technology-independent representation into a technology-dependent one given a library of cells. Even if technology libraries contain multi-output cells, state-of-the-art techniques fully exploit single-output cells only. Mul ...

2023

Thermo-hydro-mechanical behavior of energy barrettes: Field experiments and numerical simulations

Lyesse Laloui, Alessandro Francesco Rotta Loria, Elena Ravera

Over the past two decades, the thermo-hydro-mechanical behavior of earth-contact structures such as piles, walls, slabs, and tunnels, which simultaneously provide structural support and energy supply, has been studied through various field experiments and ...

ELSEVIER2023

A Versatile Mapping Approach for Technology Mapping and Graph Optimization

Giovanni De Micheli, Heinz Riener, Alessandro Tempia Calvino, Shubham Rai, Akash Kumar

This paper proposes a versatile mapping approach that has three objectives: i) it can map from one technology-independent graph representation to another; ii) it can map to a cell library; iii) it supports logic rewriting. The method is cut-based, mitigate ...

IEEE2022

Slim: Explicit Slot-Intent Mapping With Bert For Joint Multi-Intent Detection And Slot Filling

Boi Faltings, Fei Mi, Fengyu Cai, Wanhao Zhou

Utterance-level intent detection and token-level slot filling are two key tasks for spoken language understanding (SLU) in task-oriented systems. Most existing approaches assume that only a single intent exists in an utterance. However, there are often mul ...

IEEE2022

Micro-addition of Fe in highly alloyed Cu-Ti alloys to improve both formability and strength

Cyril Cayron, Roland Logé, Baptiste Thomas Jean Rouxel

Cu-Be alloys provide excellent electrical and mechanical properties, but present serious health hazards during manufacturing. Among alternative alloys, the Cu-Ti system has the highest yield strength; however, Ti cannot be easily solutionized at concentrat ...

ELSEVIER SCI LTD2022

Formula Normalizations in Verification

Viktor Kuncak, Mario Bucev, Simon Guilloud, Dragana Milovancevic

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

2023

Orchestration of oscillatory activity to improve visual motion discrimination

Roberto Felipe Salamanca Giron

This thesis describes advances in the use of novel configurations of non-invasive brain stimulation over the visual system allowing to modulate of modifying electro-physiological activity, interregional interactions and by it, visual behavior such as motio ...

EPFL2021

On the adjustment, calibration and orientation of drone photogrammetry and laser-scanning

Emmanuel Pierre Quentin Clédat

Centimetre level precision mapping is essential for many applications such as land-use, infrastructure inspection, cultural heritage preservation, and construction site monitoring. However, the acquisition and its preparation (in particular the setting of ...

EPFL2020

Better Patch Stitching for Parametric Surface Reconstruction

Pascal Fua, Mathieu Salzmann, Jan Bednarík, Zhantao Deng

Recently, parametric mappings have emerged as highly effective surface representations, yielding low reconstruction error. In particular, the latest works represent the target shape as an atlas of multiple mappings, which can closely encode object parts. A ...

IEEE2020

Financing Biomedical Ventures - Myths and Realities

Jeffrey Scott Behrens

Angel funding is an important source of capital for startup ventures (J. Sohl 2019), providing a similar level of capital as institutional venture capital (OECD 2011). But angel funding is challenging to study due to the informal nature of the activity. A ...

EPFL2020

Omnidirectional Strategies for Exploring Ancient Cities and Territories

Sarah Irene Brutton Kenderdine

By focusing on technologies of virtual reality in conjunction with theories of “place” and “presence,” this chapter outlines the importance of new approaches to the museological experience and exploration of ancient cities and cultural heritage sites. Expl ...

Oxford University Press2020

Complete coordination of robotic fiber positioners for massive spectroscopic surveys

Denis Gillet, Jean-Paul Richard Kneib, Matin Macktoobian

Robotic fiber positioners play a vital role in the generation of massive spectroscopic surveys. The more complete a positioners set is coordinated, the more information its corresponding spectrograph receives during an observation. The complete coordinatio ...

2019

On the effect of ligand shell heterogeneity on nanoparticle/protein binding thermodynamics

Francesco Stellacci, Ahmet Bekdemir, Suiyang Liao

Nonspecific protein adhesion to nanoparticle (NP) has been proven to have important implications in nanomedicine. However, there are only a few examples of careful studies relating protein binding thermodynamics to NP physicochemical features. In particula ...

2019

Biomimetic adaptive control of a deployable tensegrity structure

Ann Christine Sychterz

Biomimetic behavior includes aspects such as learning from previous experience, self-diagnosis, and adaptation. This thesis describes control methodologies that are essential to development towards biomimetic behavior of a complex deployable structure. Sim ...

EPFL2018

A toolkit for multi-scale mapping of the solar energy-generation potential of buildings in urban environments under uncertainty

Emmanuel Rey, Marilyne Andersen, Parag Rastogi, Giuseppe Peronato

Many municipalities and public authorities have supported the creation of solar cadastres to map the solar energy-generation potential of existing buildings. Despite advancements in modelling solar potential, most of these tools provide simple evaluations ...

2018

Type Soundness Proofs with Definitional Interpreters

Nada Amin, Tiark Rompf

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

A Historical Review of Diachrony and Semantic Dimensions of Trace in Neurosciences and Lacanian Psychoanalysis

Pierre Magistretti

Experience leaves a trace in the nervous system through plasticity. However, the exact meaning of the mnesic trace is poorly defined in current literature. This article provides a historical review of the term trace in neuroscience and psychoanalysis liter ...

Frontiers Media2017

Essays in Bank Financing

Yalda Sigrist

This thesis examines the optimal mode of financing for banks and financial institutions. The first chapter, which is a joint work with Prof. Jean-Charles Rochet, investigates how Systemically Important Financial Institutions (SIFIs) should be financed. The ...

EPFL2017