Publications associées à Logique non classique

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

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

Architecture and Experimental Validation of a Low-Latency Phasor Data Concentrator

Mario Paolone, Asja Derviskadic, Paolo Romano, Marco Pignati

The paper presents the design principles of a Phasor Data Concentrator (PDC) that implements both the absolute and relative time data pushing logics together with a third one that aims at minimizing the latency introduced by the PDC without increasing the ...

2018

A Theory Agenda for Component-Based Design

Joseph Sifakis, Simon Bliudze

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a sem ...

Springer International Publishing2015

Cadres de vie, modes de vie et mobilités de loisirs : les vertus de la ville compacte remises en cause?

Sébastien Munafò

This thesis aims to examine the causal mechanisms of living environments on leisure mobilities and verify whether their inclusion is actually able to challenge the compact city as a sustainable urban form. The research focuses on the Swiss case and in part ...

EPFL2015

Configuration Logics: Modelling Architecture Styles

Joseph Sifakis, Simon Bliudze, Anastasia Mavridou, Eduard Baranov

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...

Springer Int Publishing Ag2015

Towards More Efficient Logic Blocks by Exploiting Biconditional Expansion

Giovanni De Micheli, Xifan Tang, Pierre-Emmanuel Julien Marc Gaillardon, Gain Kim, Luca Gaetano Amarù

Nowadays, Field Programmable Gate Arrays (FPGA) exploit Look-Up Tables (LUTs) to generate logic functions. A K-input LUT can implement any Boolean functions with K inputs. Thanks to this flexibility, LUTs remained concep ...

2015

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

Collections, Cardinalities, and Relations

Viktor Kuncak, Ruzica Piskac

Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to co ...

2010

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Analyse non-linéaire des coques géodésiques multicouches à joints semi-rigides

Julius Natterer

In the 90ies the IBOIS-EPFL developed a new kind of shell structure. The ribs were made with simple boards waved together to form a spatial rib shell. However, the engineer currently does not have any effective method to calculate these kinds of spatial st ...

EPFL2010

A Low-Power Programmable Dynamic Frequency Divider

Christian Enz

In this paper, a solution to realize a low-power programmable frequency divider using dynamic logic is proposed. By cascading compact dual-modulus divider slice with recursive feedback mechanisms, any dividing ratio is easily implemented. A 5-stages 0.18 m ...

2008