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 ...
Context. A novel high-performance exact pair-counting toolkit called fast correlation function calculator (FCFC) is presented.Aims. With the rapid growth of modern cosmological datasets, the evaluation of correlation functions with observational and simula ...
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 ...
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 ...
As it has become easier and cheaper to collect big datasets in the last few decades, designing efficient and low-cost algorithms for these datasets has attracted unprecedented attention. However, in most applications, even storing datasets as acquired has ...
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 ...
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 ...
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 ...
In order to get a better understanding of the interaction of plasma microinstabilities and associated turbulence with specific modes, an antenna is implemented in the global gyrokinetic Particle-In-Cell (PIC) code ORB5.
It consists in applying an external ...
Datacenters are the heart of our digital lives. Online applications, such as social-networking and e-commerce, run inside datacenters under strict Service Level Objectives for their tail latency. Tight latency SLOs are necessary for such services to remain ...
