Publications related to Developing Verified Software Using Leon

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Yichen Xu

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

Quantifying the Unknown: Data-Driven Approaches and Applications in Energy Systems

Paul Scharnhorst

In light of the challenges posed by climate change and the goals of the Paris Agreement, electricity generation is shifting to a more renewable and decentralized pattern, while the operation of systems like buildings is increasingly electrified. This calls ...

EPFL2024

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Scalable constrained optimization

Maria-Luiza Vladarean

Modern optimization is tasked with handling applications of increasingly large scale, chiefly due to the massive amounts of widely available data and the ever-growing reach of Machine Learning. Consequently, this area of research is under steady pressure t ...

EPFL2024

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain ...

Assoc Computing Machinery2024

Modular segmentation, spatial analysis and visualization of volume electron microscopy datasets

Martin Weigert

Volume electron microscopy is the method of choice for the in situ interrogation of cellular ultrastructure at the nanometer scale, and with the increase in large raw image datasets generated, improving computational strategies for image segmentation and s ...

Nature Portfolio2024

TSLAM: a tag-based object-centered monocular navigation system for augmented manual woodworking

Yves Weinand, Julien Gamerro, Andrea Settimi, Hong-Bin Yang

TimberSLAM (TSLAM) is an object-centered, tag-based visual self-localization and mapping (SLAM) system for monocular RGB cameras. It was specifically developed to support a robust and augmented reality pipeline for close-range, noisy, and cluttered fabrica ...

2024

Lotic-SIPCO2: Adaptation of an open-source CO2 sensor system and examination of associated emission uncertainties across a range of stream sizes and land uses

Andrew Lean Robison

River networks play a crucial role in the global carbon cycle, as relevant sources of carbon dioxide (CO2) to the atmosphere. Advancements in high-frequency monitoring in aquatic environments have enabled measurement of dissolved CO2 concentration at tempo ...

Association for the Sciences of Limnology and Oceanography (ASLO)2024

Technology-Aware Logic Synthesis for Superconducting Electronics

Giovanni De Micheli, Dewmini Sudara Marakkalage, Siang-Yun Lee, Alessandro Tempia Calvino, Mingfei Yu, Rassul Bairamkulov

Superconducting electronics provide us with cryogenic digital circuits that can rival established technologies in performance and energy consumption. Today, the lack of tools for the design of large-scale integrated superconducting circuits is a major obst ...

2024

Scalable Logic Rewriting Using Don’t Cares

Giovanni De Micheli, Alessandro Tempia Calvino

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

2024

Toward Reliable Human Pose Forecasting With Uncertainty

Alexandre Massoud Alahi, Saeed Saadatnejad, Taylor Ferdinand Mordan, Parham Saremi

Recently, there has been an arms race of pose forecasting methods aimed at solving the spatio-temporal task of predicting a sequence of future 3D poses of a person given a sequence of past observed ones. However, the lack of unified benchmarks and limited ...

2024

Automated all-functionals infrared and Raman spectra

Nicola Marzari, Lorenzo Bastonero

Infrared and Raman spectroscopies are ubiquitous techniques employed in many experimental laboratories, thanks to their fast and non-destructive nature able to capture materials' features as spectroscopic fingerprints. Nevertheless, these measurements freq ...

Nature Portfolio2024

Generalizing Bulk-Synchronous Parallel Processing for Data Science: From Data to Threads and Agent-Based Simulations

Zilu Tian

Agent-based simulations have been widely applied in many disciplines, by scientists and engineers alike. Scientists use agent-based simulations to tackle global problems, including alleviating poverty, reducing violence, and predicting the impact of pandem ...

EPFL2023

Multiparty Homomorphic Encryption: from Theory to Practice

Christian Vincent Mouchet

Multiparty homomorphic encryption (MHE) enables a group of parties to encrypt data in a way that (i) enables the evaluation of functions directly over its ciphertexts and (ii) enforces a joint cryptographic access-control over the underlying data. By exten ...

EPFL2023

Practical Implementations of Remote Power Side-Channel and Fault-Injection Attacks on Multitenant FPGAs

Francesco Regazzoni, Mirjana Stojilovic, Ognjen Glamocanin, Dina Gamaleldin Ahmed Shawky Mahmoud

Cloud computing environments increasingly provision FPGAs because of their fine-grained, highly parallel, and flexible hardware architecture. The availability of FPGAs in the cloud fueled research on the security risks associated with exposing FPGA fabric ...

Springer, Cham2023

Projector-based augmented stacking framework for irregularly shaped objects

Yves Weinand, Katrin Beyer, Julien Gamerro, Andrea Settimi, Qianqing Wang, Edward Carlo Giorgio Andò

Augmented reality in additive fabrication is predominantly applied to the manufacturing of structures from regularly shaped materials. Our work however embraces natural heterogeneity, by focusing on the assembly of irregularly shaped elements such as miner ...

2023

Advancing atomic force microscopy through open source instrumentation

Mustafa Kangül

Atomic force microscopy (AFM), a member of the scanning probe microscopy (SPM) family, holds a unique position as a nano-characterization instrument in the fields of physics, chemistry, and biology. Its ability to provide atomic resolution and operate in v ...

EPFL2023

Quality-Constrained Encoding Optimization for Omnidirectional Video Streaming

Pascal Frossard, Roberto Gerson De Albuquerque Azevedo, Chaofan He

Omnidirectional video streaming is usually implemented based on the representations of tiles, where the tiles are obtained by splitting the video frame into several rectangular areas and each tile is converted into multiple representations with different r ...

Ieee-Inst Electrical Electronics Engineers Inc2023

Deep Generative Models for Autonomous Driving: from Motion Forecasting to Realistic Image Synthesis

Saeed Saadatnejad

Forecasting is a capability inherent in humans when navigating. Humans routinely plan their paths, considering the potential future movements of those around them. Similarly, to achieve comparable sophistication and safety, autonomous systems must embrace ...

EPFL2023

Blue Brain Nexus: An open, secure, scalable system for knowledge graph management and data-driven science

Henry Markram, Henry Genet, Alejandra Garcia Rojas Martinez, Sean Lewis Hill, Huanxiang Lu, Mohameth François Sy, Samuel Claude Kerrien, Michaël Fernand Paul Dupont, Silvia Rosario Jimenez Tejeda, Bogdan Roman, Ian Lavriushev, Anna-Kristin Kaufmann, Didac Montero Mendez, Wojciech Adam Wajerowicz, Pierre-Alexandre Fonta, Kenneth William Pirman, Julien Antonin Machon, Jonathan Raël Lurie, Dhanesh Neela Mana, Natalia Stafeeva, Alexander Désiré Ulbrich, Carolina Johanna Elisabeth Lindqvist

Modern data-driven science often consists of iterative cycles of data discovery, acquisition, preparation, analysis, model building and validation leading to knowledge discovery as well as dissemination at scale. The unique challenges of building and simul ...

2023