Publication

Extending Safe C Support In Leon

Publications associées (79)

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

Creating Trust by Abolishing Hierarchies

Mathias Josef Payer, Edouard Bugnion, Evangelos Marios Kogias, Adrien Ghosn, Charly Nicolas Lucien Castes, Neelu Shivprakash Kalani, Yuchen Qian

Software is going through a trust crisis. Privileged code is no longer trusted and processes insufficiently protect user code from unverified libraries. While usually treated separately, confidential computing and program compartmentalization are both symp ...

Association for Computing Machinery2023

On Verified Scala for STIX File System Embedded Code using Stainless

Viktor Kuncak, Jad Hamza

We present an approach for using formal methods in embedded systems and its evaluation on a case study. In our approach, the developers describe the system in a restricted subset of the high-level programming language Scala. We then use 1) a verification s ...

2022

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Yichen Xu, Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

New York2022

Automated Verification of Network Function Binaries

George Candea, Solal Vincenzo Pirelli

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

USENIX Association2022

Formal Verification of Rust with Stainless

Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...

2021

Hardware-Software Co-Design of an RPC Processor

Arash Pourhabibi Zarandi

The booming popularity of online services has led to a major evolution in the way these services are built and deployed. To cope with such online data-intensive services, service providers deploy several massive-scale datacenters, also referred to as wareh ...

EPFL2021

Given the increasing ubiquity of online embedded devices, analyzing their firmware is important to security, privacy, and safety. The tight coupling between hardware and firmware and the diversity found in embedded systems makes it hard to perform dynamic ...

USENIX ASSOC2020

, , , ,

The eective deployment of Phasor Measurement Units (PMUs) in Distribution Networks (DNs) requires an enhancement in terms of estimation accuracy beyond the limits of IEEE Std C37.118.1 (IEEE Std), aiming at a Total Vector Error (TVE) in the order of 0.0x% ...

2019

Code verification is an important part of software development process that asserts code correctness. In this work, analytical solutions are used in order to develop a simple multiphysics problem involving coupled fluid dynamics and neutron transport to be ...

2018

Modern software systems heavily use the memory heap. As systems grow more complex and compute with increasing amounts of data, it can be difficult for developers to understand how their programs actually use the bytes that they allocate on the heap and whe ...

ACM2018