Publications associées à Formal specification

Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Yichen Xu, Aleksander Slawomir Boruch-Gruszecki

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

Chat2Code: A Chatbot for Model Specification and Code Generation, The Case of Smart Contracts

Shailesh Mishra

The potential of automatic code generation through Model-Driven Engineering (MDE) frameworks has yet to be realized. Beyond their ability to help software professionals write more accurate, reusable code, MDE frameworks could make programming accessible fo ...

Ieee Computer Soc2023

Sampling of alternatives in migration aspiration models

Michel Bierlaire, Evangelos Paschalidis

The use of discrete choice models (DCMs) is a regular approach to investigating migration aspirations concerning destination choices. However, given the complex substitution patterns between destinations, more advanced model specifications than the multino ...

2023

Decentralized in-order execution of a sequential task-based code for shared-memory architectures

Charly Nicolas Lucien Castes

The hardware complexity of modern machines makes the design of adequate programming models crucial for jointly ensuring performance, portability, and productivity in high-performance computing (HPC). Sequential task-based programming models paired with adv ...

IEEE COMPUTER SOC2022

Automated Verification of Network Function Binaries

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki

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

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Overcoming decision paralysis—A digital twin for decision making in energy system design

François Maréchal, Julia Granacher, Tuong-Van Nguyen

The design of efficient energy systems, through the development of new technologies and the improvement of current ones, requires the use of rigorous process synthesis methods for generating and analysing design alternatives. We introduce a digital twin of ...

2022

Direct Model-checking of SysML Models

Alessandro Tempia Calvino

Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a ne ...

SCITEPRESS2021

A Simpler and Faster NIC Driver Model for Network Functions

George Candea, Solal Vincenzo Pirelli

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that p ...

2021

Data-Driven Convergence Prediction of Astrobots Swarms

Denis Gillet, Jean-Paul Richard Kneib, Matin Macktoobian, Francesco Basciani

Astrobots are robotic artifacts whose swarms are used in astrophysical studies to generate the map of the observable universe. These swarms have to be coordinated with respect to various desired observations. Such coordination\footnote{\z{A coordination sa ...

2022

Learning convergence prediction of astrobots in multi-object spectrographs

Denis Gillet, Jean-Paul Richard Kneib, Matin Macktoobian, Francesco Basciani

Astrobot swarms are used to capture astronomical signals to generate the map of the observable universe for the purpose of dark energy studies. The convergence of each swarm in the course of its coordination has to surpass a particular threshold to yield a ...

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

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

Verifying Software Network Functions with No Verification Expertise

George Candea, Solal Vincenzo Pirelli, Rishabh Ramesh Iyer, Aikaterini Argyraki, Luis David Figueiredo Mascarenhas Moreira Pedrosa, Matteo Rizzo

We present the design and implementation of Vigor, a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Developers write ...

ACM2019

Formal Analysis of Human-Assisted Smart City Emergency Services

Mohammad Khaja Nazeeruddin

The concept of IoT-based Smart Cities has gained momentum in recent years. The research in this domain has focused on modeling key characteristics of future smart cities along with exploring their design and implementation aspects from multiple perspective ...

2019

Formal Analysis of Distance Bounding with Secure Hardware

Serge Vaudenay, Handan Kilinç Alper

A distance bounding (DB) protocol is a two-party authentication protocol between a prover and a verifier which is based on the distance between the prover and the verifier. It aims to defeat threats by malicious provers who try to convince that they are cl ...

2018

Optimized Data Representation for Interactive Multiview Navigation

Pascal Frossard, Thomas Maugey, Rui Ma

In contrary to traditional media streaming services where a unique media content is delivered to different users, interactive multiview navigation applications enable users to choose their own viewpoints and freely navigate in a three-dimensional scene. Th ...

2018

A Time-Vertex Signal Processing Framework

Nathanaël Perraudin, Benjamin Ricaud, Andreas Loukas, Francesco Grassi

An emerging way to deal with high-dimensional non-euclidean data is to assume that the underlying structure can be captured by a graph. Recently, ideas have begun to emerge related to the analysis of time-varying graph signals. This work aims to elevate th ...

Institute of Electrical and Electronics Engineers2018

Exogenous Coordination of Concurrent Software Components with JavaBIP

Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, Alina Zolotukhina

A strong separation of concerns is necessary in order to make the design of domain-specific functional components independent from cross-cutting concerns, such as concurrent access to the shared resources of the execution platform. Native coordination mech ...

Wiley-Blackwell2017