Publications related to Lazy Shape Analysis

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.

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

Graph Neural Networks (GNNs) have emerged as a powerful tool for learning on graphs, demonstrating exceptional performance in various domains. However, as GNNs become increasingly popular, new challenges arise. One of the most pressing is the need to ensur ...

This work presents a graph neural network (GNN) framework for solving the maximum independent set (MIS) problem, inspired by dynamic programming (DP). Specifically, given a graph, we propose a DP-like recursive algorithm based on GNNs that firstly construc ...

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

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

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

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

The field of computational topology has developed many powerful tools to describe the shape of data, offering an alternative point of view from classical statistics. This results in a variety of complex structures that are not always directly amenable for ...

In several machine learning settings, the data of interest are well described by graphs. Examples include data pertaining to transportation networks or social networks. Further, biological data, such as proteins or molecules, lend themselves well to graph- ...

Consider the family of bounded degree graphs in any minor-closed family (such as planar graphs). Let d be the degree bound and n be the number of vertices of such a graph. Graphs in these classes have hyperfinite decompositions, where, one removes a small ...

Suppose that the vertices of a graph G are colored with two colors in an unknown way. The color that occurs on more than half of the vertices is called the majority color (if it exists), and any vertex of this color is called a majority vertex. We study th ...

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

Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a ne ...

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

We propose GoldFinger, a new compact and fast-to-compute binary representation of datasets to approximate Jaccard’s index. We illustrate the effectiveness of GoldFinger on the emblematic big data problem of K-Nearest-Neighbor (KNN) graph construction and s ...

Binary logic operations are the building blocks of computing machines. In this paper, we present a new programmable binary logic gate based on programmable multistable mechanisms (PMM), which are multistable structures whose stability behavior depends on m ...

The inception of object-oriented programming introduces a category of bugs related to object construction: initialization errors. Every newly created object goes through several initialization states: starting from a state where all fields are uninitialize ...

The emerging field of graph signal processing (GSP) allows one to transpose classical signal processing operations (e.g., filtering) to signals on graphs. The GSP framework is generally built upon the graph Laplacian, which plays a crucial role in studying ...

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

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

Lazy Shape Analysis

Chat with Graph Search

Acceleration of graph pattern mining and applications to financial crime

Privacy-Preserving Machine Learning on Graphs

Maximum Independent Set: Self-Training through Dynamic Programming

Scaling Language Features for Program Verification

Automated Verification of Network Function Binaries

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

Synthetic Disinformation Attacks on Automated Fact Verification Systems

Reduced representations of complexes, signals, and multifiltrations

Graph Representation Learning with Optimal Transport: Analysis and Applications

Random walks and forbidden minors III: poly(d epsilon(-1))-time partition oracles for minor-free graph classes

Adaptive majority problems for restricted query graphs and for weighted sets

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

Direct Model-checking of SysML Models

Verification of Software Network Functions with No Verification Expertise

Smaller, Faster & Lighter KNN Graph Constructions

Programmable Logic Gates Based On Tunable Multistable Mechanisms

Safe initialization of objects

Community-Aware Graph Signal Processing: Modularity Defines New Ways of Processing Graph Signals

Verified Functional Programming

Scaling Functional Synthesis and Repair