Publication

Verifying and Synthesizing Software with Recursive Functions

Publications associées (28)

BMAT: An open-source BIDS managing and analysis tool

Meritxell Bach Cuadra, Benoît Macq, Francesco La Rosa, Maxence Charles F Wynen

Magnetic Resonance Imaging (MRI) is an established technique to study in vivo neurological disorders such as Multiple Sclerosis (MS). To avoid errors on MRI data organization and automated processing, a standard called Brain Imaging Data Structure (BIDS) h ...

ELSEVIER SCI LTD2022

Automated Design: A Journey Across Modelling, Optimization, and Education

Cyril Picard

Machine intelligence greatly impacts almost all domains of our societies. It is profoundly changing the field of mechanical engineering with new technical possibilities and processes. The education of future engineers also needs to adapt in terms of techni ...

EPFL2021

Algebraic and Boolean Optimization Methods for AQFP Superconducting Circuits

Giovanni De Micheli, Eleonora Testa, Heinz Riener, Siang-Yun Lee

Adiabatic quantum-flux-parametron (AQFP) circuits are a family of superconducting electronic (SCE) circuits that have recently gained growing interest due to their low-energy consumption, and may serve as alternative technology to overcome the down-scaling ...

IEEE2021

Proving and Disproving Equivalence of Functional Programming Assignments

Viktor Kuncak, Dragana Milovancevic

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

2023

On the ‘cultural transfer’ of modern architecture northwards - Akzeptiere: Das Buch und seine Geschichte

Chiara Monterumisi

"Akzeptiere: Das Buch und seine Geschichte" is the latest in-depth contribution by Atli Magnus Seelow, one of several by him on the 1930 Stockholm exhibition and the book accepetera, the 200-page text often referred to as ‘the manifesto of Swedish function ...

2021

High-Level Synthesis of Dynamically Scheduled Circuits

Lana Josipovic

High-Level Synthesis (HLS) tools generate hardware designs from high-level programming languages. These tools almost universally build datapaths that are controlled using a centralized controller which relies on a static, compile-time schedule to determine ...

EPFL2021

Three-Input Gates for Logic Synthesis

Giovanni De Micheli, Eleonora Testa, Mathias Soeken, Dewmini Sudara Marakkalage, 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

Personalizable computational models of electrical spinal cord stimulation to restore function after neurological disorders

Andreas Rowald

Spinal Cord Injury (SCI) disrupts the communication between the brain and spinal circuits below the lesion, leading to a plethora of neurological impairments, including the loss of motor function. At present, the only medical practices to enhance recovery ...

EPFL2021