Concept

Runtime verification

Related publications (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

Efficient Verifiable Delay Functions

Benjamin Pierre Charles Wesolowski

We construct a verifiable delay function (VDF). A VDF is a function whose evaluation requires running a given number of sequential steps, yet the result can be efficiently verified. They have applications in decentralised systems, such as the generation of ...

SPRINGER INTERNATIONAL PUBLISHING AG2019

SAT Based Exact Synthesis using DAG Topology Families

Giovanni De Micheli, Mathias Soeken, Winston Jason Haaswijk

SAT based exact synthesis is a powerful technique, with applications in logic optimization, technology mapping, and synthesis for emerging technologies. However, its runtime behavior can be unpredictable and slow. In this paper, we propose to add a new typ ...

IEEE2018

Initialization patterns in Dotty

Martin Odersky, Fengyun Liu

Safe object initialization is important to avoid a category of runtime errors in programming languages. In this paper, we provide a case study of the initialization patterns on the Dotty compiler. In particular, we find that calling dynamic-dispatching met ...

2018

Discover deeper bugs with dynamic symbolic execution and coverage-based fuzz testing

George Candea, Vitaly Chipounov, Bin Zhang, Chao Feng

Coverage-based fuzz testing and dynamic symbolic execution are both popular program testing techniques. However, on their own, both techniques suffer from scalability problems when considering the complexity of modern software. Hybrid testing methods attem ...

INST ENGINEERING TECHNOLOGY-IET2018

Detailed Heap Profiling

James Richard Larus, Stuart Anthony Byma

Modern software systems heavily use the memory heap. As systems grow more complex and compute with increasing amounts of data, it can be difficult for developers to understand how their programs actually use the bytes that they allocate on the heap and whe ...

ACM2018

Cross-Platform Language Design

Sébastien Jean R Doeraene

Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model. Furthermore, they need to interact with other languages targeting said runtimes. A language targeting only one runtim ...

EPFL2018

Theory and Practice of Coroutines with Snapshots

Aleksandar Prokopec, Fengyun Liu

While event-driven programming is a widespread model for asynchronous computing, its inherent control flow fragmentation makes event-driven programs notoriously difficult to understand and maintain. Coroutines are a general control flow construct that can ...

2018

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

Existence and Uniqueness of Load-Flow Solutions in Three-Phase Distribution Networks

Jean-Yves Le Boudec, Mario Paolone, Andrey Bernstein, Cong Wang

We present sufficient conditions for the existence and uniqueness of load-flow solutions in three-phase distribution networks. The conditions can be efficiently verified for real distribution systems. ...

IEEE Institute of Electrical and Electronics Engineers2017

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017