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

Vanishing evaluations of simple functors

Jacques Thévenaz, Serge Bouc

The classification of simple biset functors is known, but the evaluation of a simple biset functor at a finite group G may be zero. We investigate various situations where this happens, as well as cases where this does not occur. We also prove a closed for ...

Elsevier2014

A Unified Formulation of Gaussian Versus Sparse Stochastic Processes-Part I: Continuous-Domain Theory

Michaël Unser, Pouya Dehghani Tafti

We introduce a general distributional framework that results in a unifying description and characterization of a rich variety of continuous-time stochastic processes. The cornerstone of our approach is an innovation model that is driven by some generalized ...

Ieee-Inst Electrical Electronics Engineers Inc2014

Analytical approximations for the collapse of an empty spherical bubble

Mohamed Farhat, Danail Obreschkow

The Rayleigh equation 3/2 (R) over dot + R(R) double over dot + p rho(-1) = 0 with initial conditions R(0) = R-0, (R) over dot(0) = 0 models the collapse of an empty spherical bubble of radius R(T) in an ideal, infinite liquid with far-field pressure p and ...

2012

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

EPFL2011

On the accuracy of approximate techniques for the evaluation of lightning electromagnetic fields along a mixed propagation path

Farhad Rachidi-Haeri, Marcos Rubinstein, Abdolhamid Shoory, Abdenabi Mimouni

In this paper we review simplified analytical expressions derived by Wait using the concept of attenuation function for the analysis of the propagation of lightning-radiated electromagnetic fields over a mixed propagation path (vertically stratified ground ...

2011

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unk ...

2008

Formal semantics for refinement verification of entreprise models

Irina Rychkova

In this dissertation we investigate how Business/IT alignment in enterprise models can be enhanced by using a software engineering stepwise refinement paradigm. To have an IT system that supports an enterprise and meets the enterprise business needs, manag ...

EPFL2008

SeamCAD: a hierarchy-oriented modeling language and a computer-aided tool for entreprise architecture

Lam Son Lê

Modeling Enterprise Architecture requires representing multiple diagrams of an enterprise, which typically shows the multiples business entities, IT systems, even software components and the services they offer. This could be done by a team of stakeholders ...

EPFL2008