Towards Complete Reasoning about Axiomatic Specifications

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assum ...

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

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

Security system designers favor worst-case security metrics, such as those derived from differential privacy (DP), due to the strong guarantees they provide. On the downside, these guarantees result in a high penalty on the system's performance. In this pa ...

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

Tissues are organized in cellular niches, the composition and interactions of which can be investigated using spatial omics technologies. However, systematic analyses of tissue composition are challenged by the scale and diversity of the data. Here we pres ...

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

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

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

There are many sources providing atmospheric weather station data for the Antarctic continent. However, variable naming, timestamps and data types are highly variable between the different sources. The published python code intends to make processing of di ...

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

The present study evaluates the ionization efficiency (IE) of linear and branched C2–C14 dicarboxylic acids (DCAs) by electrospray ionization (ESI) under different conditions. The influence of the concentration of organic modifier (MeOH); mobile phase addi ...

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

Quantification of mobility is the key to monitor the progression of mobility disorders as well as the effect of an intervention. Inertial measurement units (IMUs) with dedicated algorithms can quantify postural transitions and gait as the two key aspects o ...

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

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

The advent of the quantum computer makes current public-key infrastructure insecure. Cryptography community is addressing this problem by designing, efficiently implementing, and evaluating novel public-key algorithms capable of withstanding quantum comput ...

For decades mathematical modeling in epidemiology has helped understanding the dynamics of infectious diseases, as well as describe possible intervention scenarios to prevent and control them. However, such models were relying on several assumptions, such ...

This book defines and explores the problem of placing the instances of dynamic data types on the components of the heterogeneous memory organization of an embedded system, with the final goal of reducing energy consumption and improving performance. It is ...

Towards Complete Reasoning about Axiomatic Specifications

Chattez avec Graph Search

Mechanized HOL Reasoning in Set Theory

Automated Formal Verification of Software Network Functions

Privacy-Preserving Machine Learning on Graphs

Bayes Security: A Not So Average Metric

Capturing Types

CellCharter reveals spatial cell niches associated with tissue remodeling and cell plasticity

LISA – A Modern Proof System

On algebraic array theories

Scaling Language Features for Program Verification

Automated Verification of Network Function Binaries

Preprocessing Antarctic Weather Station (AWS) data in python

Type-Level Programming with Match Types

Standard-Free Quantification of Dicarboxylic Acids: Case Studies with Salt-Rich Effluents and Serum

NP Satisfiability for Arrays as Powers

Toward an objective assessment of mobility in clinical and daily activity settings

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

Verification of Software Network Functions with No Verification Expertise

Synthesis of Flexible Accelerators for Early Adoption of Ring-LWE Post-quantum Cryptography

Contact networks across ages: computational analysis of epidemiological dynamics

Heterogeneous Memory Organizations in Embedded Systems. Placement of Dynamic Data Objects