Deductive Synthesis and Repair

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.

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

In this work, we verify, using the Stainless program verifier, the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array. As an executable specification, we write an immutable map based on a list of tuple ...

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

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

Genome-wide chromatin conformation capture assays provide formidable insights into the spatial organization of genomes. However, due to the complexity of the data structure, their integration in multi-omics workflows remains challenging. We present data st ...

We study the homogenization of the Poisson equation with a reaction term and of the eigenvalue problem associated to the generator of multiscale Langevin dynamics. Our analysis extends the theory of two-scale convergence to the case of weighted Sobolev spa ...

Various forms of real-world data, such as social, financial, and biological networks, can be represented using graphs. An efficient method of analysing this type of data is to extract subgraph patterns, such as cliques, cycles, and motifs, from graphs. For ...

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

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC

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

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

High-level synthesis (HLS) tools typically generate statically scheduled datapaths. Static scheduling implies that the resulting circuits have a hard time exploiting parallelism in code with potential memory dependences, with control dependences, or where ...

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

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

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

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

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

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

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

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

Deductive Synthesis and Repair

Chat with Graph Search

Automated Formal Verification of Software Network Functions

Verifying a Realistic Mutable Hash Table: Case Study (Short Paper)

Transportation-based functional ANOVA and PCA for covariance operators

Degrees of Separation: A Flexible Type System for Safe Concurrency

Orchestrating chromosome conformation capture analysis with Bioconductor

Homogenization results for the generator of multiscale Langevin dynamics in weighted Sobolev spaces

Acceleration of graph pattern mining and applications to financial crime

Functional data analysis with rough sample paths?

Capturing Types

Fast correlation function calculator A high-performance pair-counting toolkit

Scaling Language Features for Program Verification

From C/C plus plus Code to High-Performance Dataflow Circuits

Automated Verification of Network Function Binaries

Type-Level Programming with Match Types

CovNet: Covariance networks for functional data on multidimensional domains

Functional peaks-over-threshold analysis

Sketches, metrics and fast algorithms

Extraction and controlled functionalization of lignin for materials applications

Covariance Estimation for Random Surfaces beyond Separability

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning