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