Publications associées à Correction d'un algorithme

On algebraic array theories

Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...

Elsevier Science Inc2023

Assessing the effect of O2 dithering on CH4 oxidation on Pd/Al2O3

Oliver Kröcher, Davide Ferri

Under periodic lean/rich operation generated by repeated O2 pulses (O2-dithering), the abatement of CH4 and NO is enhanced compared to static operation. However, it is not well understood how the dithering parameters (pulse amplitude and frequency) affect ...

ELSEVIER SCIENCE SA2023

Edit Based Grading of SQL Queries

Bikash Chandra

Grading student SQL queries manually is a tedious and error-prone process. Earlier work on testing correctness of student SQL queries, such as the XData system, can be used to test the correctness of a student query. However, in case a student query is fou ...

ASSOC COMPUTING MACHINERY2021

Proving and Disproving Equivalence of Functional Programming Assignments

Viktor Kuncak, Dragana Milovancevic

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

2023

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

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

A methodology for the rigorous verification of Particle-in-Cell simulations

Paolo Ricci, Fabio Riva, Carrie Fiona Beadle

A methodology to perform a rigorous verification of Particle-in-Cell (PIC) simulations is presented, both for assessing the correct implementation of the model equations (code verification), and evaluating the numerical uncertainty affecting the simulation ...

American Institute of Physics2017

Verification and validation procedures with applications to plasma-edge turbulence simulations

Fabio Riva

Understanding the plasma dynamics in tokamaks is of fundamental importance to reliably predict the performances of future fusion devices. Because of the complex phenomena at play, state-of-the-art simulation codes are needed to investigate the plasma dynam ...

EPFL2017

Deductive Synthesis and Repair

Etienne Kneuss

In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...

EPFL2016