Publication
Compositional verification for component-based systems and application
Publications associées (33)
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 ...
EPFL2024Automated 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 Association2022Formal 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 ...
2021Verification of Software Network Functions with No Verification Expertise
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 ...
EPFL2020Data Structures and Algorithms for Logic Synthesis in Advanced Technologies
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 ...
EPFL2020From 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. ...
ACM2018Steep 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 ...
IEEE2018Algorithmic Verification of Component-based Systems
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 ...
EPFL2017FPGAs for the Masses: Affordable Hardware Synthesis from Domain-Specific Languages
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 ...
EPFL2016Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction
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