Publications related to Towards Complete Reasoning about Axiomatic Specifications

Related publications (27)

Mechanized HOL Reasoning in Set Theory

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

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

2024

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

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

EPFL2024

Privacy-Preserving Machine Learning on Graphs

Sina Sajadmanesh

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

EPFL2023

Bayes Security: A Not So Average Metric

Carmela González Troncoso, Giovanni Cherubin

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

IEEE2023

Capturing Types

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki

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

Assoc Computing Machinery2023

Decision Procedures for Power Structures

Rodrigo Raya

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

EPFL2023

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

Albert Santamaria Martinez, Daniele Tavernari

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

Nature Portfolio2023

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

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

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

On algebraic array theories

Viktor Kuncak, Rodrigo Raya

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

Elsevier Science Inc2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

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

EPFL2022

Automated Verification of Network Function Binaries

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli

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

USENIX Association2022

Preprocessing Antarctic Weather Station (AWS) data in python

Michael Lehning, Franziska Gerber

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

Zenodo2022

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

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

ASSOC COMPUTING MACHINERY2022

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

Christian Ludwig, Daniil Salionov

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

2022

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

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

Springer, Cham2022

Virtual ADTs for Portable Metaprogramming

Martin Odersky, Nicolas Alexander Stucki

Scala 3 provides a metaprogramming interface that represents the abstract syntax tree definitions using algebraic data types. To allow the compiler to freely evolve without breaking the metaprogramming interface, we present virtual algebraic data types (or ...

ASSOC COMPUTING MACHINERY2021

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

Arash Atrsaei

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

EPFL2021

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

Maartje Martina Cornelia Bastings, Alice Comberlato

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

AMER CHEMICAL SOC2021

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

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

EPFL2020

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

Francesco Regazzoni, Subhadeep Banik

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

ASSOC COMPUTING MACHINERY2020