Full Functional Verification of Linked Data Structures

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

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

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

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

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

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

Compute memories are memory arrays augmented with dedicated logic to support arithmetic. They support the efficient execution of data-centric computing patterns, such as those characterizing Artificial Intelligence (AI) algorithms. These architectures can ...

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

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

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

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

Parsing is the process that enables a computer system to make sense of raw data. Parsing is common to almost all computer systems: It is involved every time sequential data is read and elaborated into structured data. The theory of parsing usually focuses ...

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

DNA-based nanostructures are actively gaining interest as tools for biomedical and therapeutic applications following the recent development of protective coating strategies prolonging structural integrity in physiological conditions. For tailored biologic ...

Point cloud is a promising imaging modality for the representation of 3D media. The vast volume of data associated with it requires efficient compression solutions, with lossy algorithms leading to larger bit-rate savings at the expense of visual impairmen ...

This paper presents an integrated design tool for structures composed of engineered timber panels that are connected by traditional wood joints. Recent advances in computational architecture have permitted to automate the fabrication and assembly of such s ...

Full Functional Verification of Linked Data Structures

Chat with Graph Search

Automated Formal Verification of Software Network Functions

Interpolation and Quantifiers in Ortholattices

Orthologic with Axioms

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Transportation-based functional ANOVA and PCA for covariance operators

Degrees of Separation: A Flexible Type System for Safe Concurrency

LISA – A Modern Proof System

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

Capturing Types

Overflow-free compute memories for edge AI acceleration

Scaling Language Features for Program Verification

Automated Verification of Network Function Binaries

Sketches, metrics and fast algorithms

Formula Normalizations in Verification

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

Efficient Parsing with Derivatives and Zippers

Proving and Disproving Equivalence of Functional Programming Assignments

Quantification of Strand Accessibility in Biostable DNA Origami with Single-Staple Resolution

Benchmarking of objective quality metrics for point cloud compression

An integrated design tool for timber plate structures to generate joints geometry, fabrication toolpath, and robot trajectories