Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Logique combinatoire

Publications associées (16)

Advanced Functional Decomposition Using Majority and Its Applications

Giovanni De Micheli, Mathias Soeken

Typical operators for the decomposition of Boolean functions in state-of-the-art algorithms are AND, exclusive-OR (XOR), and the 2-to-1 multiplexer (MUX). We propose a logic decomposition algorithm that uses the majority-of-three (MAJ) operation. Such a de ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2020

Measurement of Xi(++)(cc) production in pp collisions at root s=13 TeV

Jian Wang, Mingkui Wang, Olivier Schneider, Zhirui Xu, Yiming Li, Yi Zhang, Lei Zhang, Yi Wang, Aurelio Bay, Ho Ling Li, Guido Haefeli, Tatsuya Nakada, Christoph Frei, Mark Tobin, Frédéric Blanc, Maurizio Martinelli, Vladislav Balagura, Donal Patrick Hill, Liang Sun, Lesya Shchutska, François Fleuret, Mirco Dorigo, Liupan An, Renato Quagliani, Hang Yin, Guido Andreassi, Aravindhan Venkateswaran, Elena Graverini, Michel De Cian, Vladimir Macko, Federico Leo Redi, Luis Miguel Garcia Martin, Sebastian Schulte, Tommaso Colombo, Vitalii Lisovskyi, Tara Nanut, Minh Tâm Tran, Violaine Bellée, Guillaume Max Pietrzyk, Pavol Stefko, Pietro Marino, Maria Vieites Diaz, Matthieu Philippe Luther Marinangeli, Serhii Cholak, Veronica Sølund Kirsebom, Maria Elena Stramaglia, Surapat Ek-In, Ana Bárbara Rodrigues Cavalcante, Luca Pescatore, Sara Celani, Preema Rennee Pais, Maxime Schubiger, Plamen Hristov Hopchev, Carina Trippl, Thi Dung Nguyen, Alison Maria Tully, Olivier Göran Girard, Mâu Chung Nguyên, Simone Meloni, Xiaoqing Zhou, Elisabeth Maria Niel, Alexandre Brea Rodriguez

The production of Xi(++)(cc) baryons in proton-proton collisions at a centre-of-mass energy of root s = 13 Tev is measured in the transverse-momentum range 4 < p(T) < 15 GeV/c and the rapidity range 2.0 < y < 4.5. The data used in this measurement correspo ...

IOP PUBLISHING LTD2020

Structural Rewriting in XOR-Majority Graphs

Giovanni De Micheli, Mathias Soeken

In this paper, we present a structural rewriting method for a recently proposed XOR-Majority graph (XMG), which has exclusive-OR (XOR), majority-of-three (MAJ), and inverters as primitives. XMGs are an extension of Majority-Inverter Graphs (MIGs). Previous ...

ASSOC COMPUTING MACHINERY2019

Functional Decomposition Using Majority

Giovanni De Micheli, Mathias Soeken

Typical operators for the decomposition of Boolean functions in state-of-the-art algorithms are AND, exclusive-OR (XOR), and a 2-to-1 multiplexer (MUX). We propose a logic decomposition algorithm that uses the majority-of-three (MAJ) operation. Such decomp ...

IEEE2018

Monotonicity Types for Distributed Dataflow

Heather Christine Klug

The Lasp programming language provides combinator functions such as Union and Intersection for combining set CRDTs. When designing a CRDT combinator, care must be taken to ensure that the combinator is monotone separately in each of its arguments, so that ...

2017

NAND-NOR: A Compact, Fast, and Delay Balanced FPGA Logic Element

Paolo Ienne, Yu Lin, Grace Zgheib

The And-Inverter Cone has been introduced as an alternative logic element to the look-up table in FPGAs, since it improves their performance and resource utilization. However, further analysis of the AIC design showed that it suffers from the delay discrep ...

ACM2017

Implementing Higher-Kinded Types in Dotty

Martin Odersky, Dmytro Petrashko, Guillaume André Fradji Martres

dotty is a new, experimental Scala compiler based on DOT, the calculus of Dependent Object Types. Higher-kinded types are a natural extension of first-order lambda calculus, and have been a core construct of Haskell and Scala. As long as such types are jus ...

ACM2016

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015

Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

ACM2013

Accelerating Interpolants

Viktor Kuncak, Hossein Hojjat

We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), a new algorithm for verifying infinite-state transition systems. CEGAAR combines interpolation-based predicate discovery in counterexample guided predicate abstraction with accel ...

2012

Interpolation and Symbol Elimination

We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alte ...

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

Programming language abstractions for mobile code

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and suppor ...

EPFL2009

Program Analysis with Dynamic Precision Adjustment

Grégory Théoduloz

We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a ...

IEEE2008

Full Functional Verification of Linked Data Structures

Viktor Kuncak

We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify form ...

2008

The Perfectly-Synchronized Round-based Model of Distributed Computing

Rachid Guerraoui, Bastian Pochon

The perfectly-synchronized round-based model provides the powerful abstraction of crash-stop failures with atomic and synchronous message delivery. This abstraction makes distributed programming very easy.We describe a technique to automatically transform ...

2007

Lazy Shape Analysis

Grégory Théoduloz

Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analy ...

Springer2006