Concept

Runtime verification

Publications associées (26)

Latency Interfaces for Systems Code

This thesis demonstrates that it is feasible for systems code to expose a latency interface that describes its latency and related side effects for all inputs, just like the code's semantic interface describes its functionality and related side effects. S ...

EPFL2023

Synthetic Disinformation Attacks on Automated Fact Verification Systems

Antoine Bosselut

Automated fact-checking is a needed technology to curtail the spread of online misinformation. One current framework for such solutions proposes to verify claims by retrieving supporting or refuting evidence from related textual sources. However, the reali ...

ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE2022

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

DASS: Combining Dynamic & Static Scheduling in High-Level Synthesis

Paolo Ienne, Lana Josipovic

A central task in high-level synthesis is scheduling: the allocation of operations to clock cycles. The classic approach to scheduling is static, in which each operation is mapped to a clock cycle at compile-time, but recent years have seen the emergence o ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2022

Macro Modeling Technique for Integrally-Attached Timber Plates: Sensitivity Analysis

Yves Weinand, Aryan Rezaei Rad, Henry V. Burton

Using the Integral Mechanical Attachment (IMA) technique, a new macroscopic model has recently been introduced to simulate the structural behavior of segmented timber plates. The macro model is based on employing only beam and spring elements, which aims t ...

2021

A non-twisting flux tube for local gyrokinetic simulations

Stephan Brunner, Justin Richard Ball

Local gyrokinetic simulations use a field-aligned domain that twists due to the magnetic shear of the background magnetic equilibrium. However, if the magnetic shear is strong and/or the domain is long, the twist can become so extreme that it fails to prop ...

2021

Convergence of adaptive algorithms for constrained weakly convex optimization

Volkan Cevher, Ahmet Alacaoglu, Yurii Malitskyi

We analyze the adaptive first order algorithm AMSGrad, for solving a constrained stochastic optimization problem with a weakly convex objective. We prove the

\tilde O(t^{-1/2})

rate of convergence for the squared norm of the gradient of Moreau envelope, ...

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

The bias of dark matter tracers: assessing the accuracy of mapping techniques

Cheng Zhao

We present a comparison between approximated methods for the construction of mock catalogues based on the halo-bias mapping technique. To this end, we use as reference a high-resolution N-body simulation of 38403 dark matter particles on a 400 h(-1) Mpc cu ...

OXFORD UNIV PRESS2020

WOK: Statistical Program Slicing in Production

James Richard Larus, Bogdan-Alexandru Stoica

Dynamic program slicing can significantly reduce the amount of code developers need to inspect by focusing only on program statements relevant to their investigation. However, this technique is still not ready for production-level use either in terms of ru ...

IEEE2019

Convergence of adaptive algorithms for constrained weakly convex optimization

Volkan Cevher, Ahmet Alacaoglu, Yurii Malitskyi

We analyze the adaptive first order algorithm AMSGrad, for solving a constrained stochastic optimization problem with a weakly convex objective. We prove the

\tilde O(t^{-1/2})

rate of convergence for the squared norm of the gradient of Moreau envelope, ...

2021