MOOC

Parallel programming

Related publications (100)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Exact Synthesis of ESOP Forms

Giovanni De Micheli, Heinz Riener, Bruno Schmitt Antunes

We present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach finds one or more ESOP forms for a given Boolean function. The approach can dea ...

Springer2019

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

Exact Synthesis of Boolean Functions in Majority-of-five Forms

Giovanni De Micheli, Mathias Soeken, Winston Jason Haaswijk, Zhufei Chu

Recent studies show that majority-based logic synthesis is beneficial for both traditional and nanotechnology digital designs. However, most of the existing synthesis algorithms for majority logic generate majority-of-three (M-3) networks. The optimization ...

IEEE2019

Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization

Andrew James Becker

Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy various constraints. In this thesis, we demonstrate how for ...

EPFL2018

Canonical Computation without Canonical Representation

Mathias Soeken, Luca Gaetano Amarù, Ana Petkovska

A representation of a Boolean function is canonical if, given a variable order, only one instance of the representation is possible for the function. A computation is canonical if the result depends only on the Boolean function and a variable order, and do ...

IEEE2018

Verification by Reduction to Functional Programs

Régis William Blanc

In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...

EPFL2017

Exploiting Satisfiability Solvers for Efficient Logic Synthesis

Ana Petkovska

Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...

EPFL2017

Busy Man’s Synthesis: Combinational Delay Optimization With SAT

Giovanni De Micheli, Mathias Soeken

Boolean SAT solving can be used to find a minimum- size logic network for a given small Boolean function. This paper extends the SAT formulation to find a minimum-size network under delay constraints. Delay constraints are given in terms of input arrival t ...

Ieee2017

Classifying Functions with Exact Synthesis

Giovanni De Micheli, Mathias Soeken, Eleonora Testa, Winston Jason Haaswijk

Due to recent advances, constraint solvers have become efficient tools for synthesizing optimum Boolean circuits. We take advantage of this by showing how SAT based exact synthesis may be used as a method for finding minimum length Boolean chains. As oppos ...

IEEE2017

On verifying causal consistency

Rachid Guerraoui, Jad Hamza

Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automaticall ...