Publication

On algebraic array theories

Viktor Kuncak, Rodrigo Raya
2023
Journal Articles

Abstract

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. The method is applied to obtain an extension of combinatory array logic that is closed under propositional operations and Hoare triples. A classification according to expressiveness of six different fragments studied in the literature is given.(c) 2023 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).

Official source

https://infoscience.epfl.ch/entities/publication/9afa3a14-1eda-47fd-9fc3-0df2981327b1

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Viktor Kuncak, Rodrigo Raya
2023
Journal Articles

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/9afa3a14-1eda-47fd-9fc3-0df2981327b1

About this result

Related concepts (24)

MIT License

The MIT License is a permissive free software license originating at the Massachusetts Institute of Technology (MIT) in the late 1980s. As a permissive license, it puts only very limited restriction on reuse and has, therefore, high license compatibility. Unlike copyleft software licenses, the MIT License also permits reuse within proprietary software, provided that all copies of the software or its substantial portions include a copy of the terms of the MIT License and also a copyright notice.

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program. In functional programming, functions are treated as first-class citizens, meaning that they can be bound to names (including local identifiers), passed as arguments, and returned from other functions, just as any other data type can.

Propositional formula

In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional formula may also be called a propositional expression, a sentence, or a sentential formula. A propositional formula is constructed from simple propositions, such as "five is greater than three" or propositional variables such as p and q, using connectives or logical operators such as NOT, AND, OR, or IMPLIES; for example: (p AND NOT q) IMPLIES (p OR q).

Related publications (28)

Quantitative convergence rates for scaling limit of SPDEs with transport noise

Lucio Galeati

We consider on the torus the scaling limit of stochastic 2D (inviscid) fluid dynamics equations with transport noise to deterministic viscous equations. Quantitative estimates on the convergence rates are provided by combining analytic and probabilistic ar ...

Academic Press Inc Elsevier Science2024

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

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

Association for Computing Machinery2024

The connection of the acyclic disconnection and feedback arc sets - On an open problem of Figueroa et al

Lukas Fritz Felix Vogl

We examine the connection of two graph parameters, the size of a minimum feedback arcs set and the acyclic disconnection. A feedback arc set of a directed graph is a subset of arcs such that after deletion the graph becomes acyclic. The acyclic disconnecti ...

Elsevier2024