Publication

Compositional verification for component-based systems and application

Publications associées (33)

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

Exploring High-Performance and Energy-Efficient Architectures for Edge AI-Enabled Applications

Joshua Alexander Harrison Klein

The desire and ability to place AI-enabled applications on the edge has grown significantly in recent years. However, the compute-, area-, and power-constrained nature of edge devices are stressed by the needs of the AI-enabled applications, due to a gener ...

EPFL2024

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

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

Data Structures and Algorithms for Logic Synthesis in Advanced Technologies

Eleonora Testa

Logic synthesis is a key component of digital design and modern EDA tools; it is thus an essential instrument for the design of leading-edge chips and to push the limits of their performance. In the last decades, the electronic circuits community has evolv ...

EPFL2020

From Uncertainty Data to Robust Policies for Temporal Logic Planning

Maryam Kamgarpour, Tony Alan Wood

We consider the problem of synthesizing robust disturbance feedback policies for systems performing complex tasks. We formulate the tasks as linear temporal logic specifications and encode them into an optimization framework via mixed-integer constraints. ...

ACM2018

Steep Slope Transistors for Quantum Computing

Mihai Adrian Ionescu, Teodor Rosca, Cem Alper

In this paper we will present and discuss the potential of steep slope transistors to serve at cryogenic temperature: (i) the electronic design that is needed for qubit error correction and/or interfacing and (ii) to serve as ultra-sensitive charge detecto ...

IEEE2018

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

FPGAs for the Masses: Affordable Hardware Synthesis from Domain-Specific Languages

Nithin George

Field Programmable Gate Arrays (FPGAs) have the unique ability to be configured into application-specific architectures that are well suited to specific computing problems. This enables them to achieve performances and energy efficiencies that outclass oth ...

EPFL2016

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015