Publications associées à Formule logique

Orthologic with Axioms

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

Formula Normalizations in Verification

Viktor Kuncak, Simon Guilloud, Mario Bucev, Dragana Milovancevic

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

2023

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

The Gray-Wyner Network and Wyner's Common Information for Gaussian Sources

Michael Christoph Gastpar, Erixhen Sula

This paper presents explicit solutions for two related non-convex information extremization problems due to Gray and Wyner in the Gaussian case. The first problem is the Gray-Wyner network subject to a sum-rate constraint on the two private links. Here, ou ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2022

Three-Input Gates for Logic Synthesis

Giovanni De Micheli, Mathias Soeken, Dewmini Sudara Marakkalage, Eleonora Testa, Heinz Riener

Most logic synthesis algorithms work on graph representations of logic functions with nodes associated with arbitrary logic expressions or simple logic functions and iteratively optimize such graphs. While recent multilevel logic synthesis efforts focused ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2021

Universal Sparse Superposition Codes With Spatial Coupling and GAMP Decoding

Nicolas Macris, Jean François Emmanuel Barbier, Mohamad Baker Dia

Sparse superposition codes, or sparse regression codes, constitute a new class of codes, which was first introduced for communication over the additive white Gaussian noise (AWGN) channel. It has been shown that such codes are capacity-achieving over the A ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2019

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

2017

Elliptic curves over a finite field and the trace formula

Ian Nicholas Petrow

We prove formulas for power moments for point counts of elliptic curves over a finite field k such that the groups of k-points of the curves contain a chosen subgroup. These formulas express the moments in terms of traces of Hecke operators for certain con ...

Wiley2017

The Critical Shear Crack Theory for punching design: from a mechanical model to closed-form design expressions

Aurelio Muttoni, Miguel Fernández Ruiz

The Critical Shear Crack Theory (CSCT) is a consistent approach used for shear design of one- and two-way slabs failing in shear and punching shear respectively. The theory is based on a mechanical model allowing to determine the amount of shear force that ...

2016

On the design of unit-cells for acoustic metasurfaces

Hervé Lissek, Sami Driss Karkar, Seyyed Hussein Seyyed Esfahlani

Acoustic metasurfaces have gained popularity for their capability to tailor the phase front of transmitted and reflected waves. While most of researches conducted in this topic are spinning around different applications and peculiar physics of these surfac ...

IEEE2015