Deductive Program Repair, Computer Aided Verification

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Functional data are typically modeled as sample paths of smooth stochastic processes in order to mitigate the fact that they are often observed discretely and noisily, occasionally irregularly and sparsely. The smoothness assumption is imposed to allow for ...

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 ...

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 ...

We consider the problem of comparing several samples of stochastic processes with respect to their second-order structure, and describing the main modes of variation in this second order structure, if present. These tasks can be seen as an Analysis of Vari ...

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 ...

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 ...

Covariance estimation is ubiquitous in functional data analysis. Yet, the case of functional observations over multidimensional domains introduces computational and statistical challenges, rendering the standard methods effectively inapplicable. To address ...

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 ...

Peaks-over-threshold analysis using the generalised Pareto distribution is widely applied in modelling tails of univariate random variables, but much information may be lost when complex extreme events are studied using univariate results. In this paper, w ...

Lignin is a renewable aromatic polymer that due to its abundance and unique chemical structure is a promising candidate to replace aromatic materials that are currently sourced from fossil oil. The same structure of lignin poses however drawbacks for its v ...

Computational thinking (CT) skills are becoming increasingly relevant for future professionals across all domains, beyond computer science (CS). As such, an increasing number of bachelor and masters programs outside of the computer science discipline integ ...

This thesis focuses on non-parametric covariance estimation for random surfaces, i.e.~functional data on a two-dimensional domain. Non-parametric covariance estimation lies at the heart of functional data analysis, and considerations of statistical and com ...

The performance of programs written in languages following the dataflow model of computation (MoC) largely depends on the configuration (partitioning, mapping, scheduling, buffer dimensioning) chosen during the synthesis stages. Furthermore, this programmi ...

How can we discern whether the covariance operator of a stochastic pro-cess is of reduced rank, and if so, what its precise rank is? And how can we do so at a given level of confidence? This question is central to a great deal of methods for functional dat ...

Programming has changed; programming languages have not. Modern software embraced reusable software components, i.e., public libraries, and runs in the cloud, on machines that co-locate applications from various origins. This new programming paradigm leads ...

We develop theory and methodology for the problem of nonparametric registration of functional data that have been subjected to random deformation (warping) of their time scale. The separation of this phase variation ("horizontal" variation) from the amplit ...

Programming with monads can be advantageous even in imperative languages with builtin support for side effects. However, in these languages composing monadic programs is different from composing side effecting imperative programs. This does not need to be ...

Non-Volatile Memory (NVM) is an emerging type of memory device that provides fast, byte-addressable, and high-capacity durable storage. NVM sits on the memory bus and allows durable data structures designs similar to the in-memory equivalent ones. Expensiv ...

The analysis of nuclear reactors for performance and safety assessment benefits from the use of computational tools. In this context, this work aims at the development and application of a thermal-hydraulics methodology and related software that respond to ...

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 ...

Deductive Program Repair, Computer Aided Verification

Chat with Graph Search

Functional data analysis with rough sample paths?

Automated Formal Verification of Software Network Functions

Degrees of Separation: A Flexible Type System for Safe Concurrency

Transportation-based functional ANOVA and PCA for covariance operators

Proving and Disproving Equivalence of Functional Programming Assignments

Scaling Language Features for Program Verification

CovNet: Covariance networks for functional data on multidimensional domains

Automated Verification of Network Function Binaries

Functional peaks-over-threshold analysis

Extraction and controlled functionalization of lignin for materials applications

Promoting Computational Thinking Skills in Non-Computer Science Students Gamifying Computational Notebooks to Increase Student Engagement

Covariance Estimation for Random Surfaces beyond Separability

Performance Estimation of High-Level Dataflow Program on Heterogeneous Platforms

Testing For The Rank Of A Covariance Operator

Trust as a Programming Primitive

Functional registration and local variations: Identifiability, rank, and tuning

Representing Monads with Capabilities

Software Support for Non-Volatile Memory (NVM) Programming

A Coarse-mesh Methodology for the Analysis of One and Two-phase Nuclear Reactor Thermal-hydraulics in a Multi-physics Context

Verification of Software Network Functions with No Verification Expertise