Publications related to Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet

Related publications (15)

FlexiMem: Flexible Shared Virtual Memory for PCIe-attached FPGAs

Paolo Ienne, Canberk Sönmez, Mohamed Mahfouz Ahmed Kotb Shahawy, Cemalettin Cem Belentepe

Shared Virtual Memory (SVM) is a mechanism that allows host-side applications and FPGA accelerators to access the same virtual address space. It enables accelerating algorithms with unpredictable memory access patterns by making transparent pointer sharing ...

Institute of Electrical and Electronics Engineers Inc.2024

Error Resilient In-Memory Computing Architecture for CNN Inference on the Edge

David Atienza Alonso, Giovanni Ansaloni, Alexandre Sébastien Julien Levisse, Flavio Ponzina, Marco Antonio Rios

The growing popularity of edge computing has fostered the development of diverse solutions to support Artificial Intelligence (AI) in energy-constrained devices. Nonetheless, comparatively few efforts have focused on the resiliency exhibited by AI workload ...

2022

PROFACTORY: Improving IoT Security via Formalized Protocol Customization

Mathias Josef Payer

As IoT applications gain widespread adoption, it becomes important to design and implement IoT protocols with security. Existing research in protocol security reveals that the majority of disclosed protocol vulnerabilities are caused by incorrectly impleme ...

USENIX ASSOC2022

Rebooting Virtual Memory with Midgard

Babak Falsafi, Mathias Josef Payer, Siddharth Gupta, Atri Bhattacharyya, Yunho Oh, Abhishek Bhattacharjee

Computer systems designers are building cache hierarchies with higher capacity to capture the ever-increasing working sets of modern workloads. Cache hierarchies with higher capacity improve system performance but shift the performance bottleneck to addres ...

2021

Self-Organized Laboratories for Smart Campus

Denis Gillet, Christophe Salzmann

A smart campus provides students who are geographically scattered with online tools to get access to learning resources and laboratories. Although these remote laboratories have the potential and capabilities to implement different learning experiments, mo ...

IEEE COMPUTER SOC2020

A Hybrid Cache HW/SW Stack for Optimizing Neural Network Runtime, Power and Endurance

David Atienza Alonso, Marina Zapater Sancho, Alexandre Sébastien Julien Levisse, William Andrew Simon

Hybrid caches consisting of both SRAM and emerging Non-Volatile Random Access Memory (eNVRAM) bitcells increase cache capacity and reduce power consumption by taking advantage of eNVRAM's small area footprint and low leakage energy. However, they also inhe ...

2020

Computational characteristics and hardware implications of brain tissue simulations

Francesco Cremonesi

Understanding the link between the brain's anatomy and its function through computer simulations of neural tissue models is a widely used approach in computational neuroscience. This technique enables rapid prototyping and testing of hypotheses, allowing r ...

EPFL2019

Exact Synthesis of LTL Properties from Traces

Heinz Riener

We present an exact approach to synthesize temporal-logic formulas in linear temporal logic (LTL) from a set of given positive and negative example traces. Our approach uses topology structures, in particular partial DAGs, to partition the search space int ...

IEEE2019

Placement of Virtual Containers on NUMA systems: A Practical and Comprehensive Model

Baptiste Joseph Eustache Lepers

Our work addresses the problem of placement of threads, or virtual cores, onto physical cores in a multicore NUMA system. Different placements result in varying degrees of contention for shared resources, so choosing the right placement can have a large ef ...

USENIX ASSOC2018

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

New Data Structures and Algorithms for Logic Synthesis and Verification

Luca Gaetano Amarù

The strong interaction between Electronic Design Automation (EDA) tools and Complementary Metal-Oxide Semiconductor (CMOS) technology contributed substantially to the advancement of modern digital electronics. The continuous downscaling of CMOS Field Effec ...

EPFL2015

Systematically testing OpenFlow controller applications

Dejan Kostic, Marco Canini, Peter Peresini, Maciej Leszek Kuzniar

The emergence of OpenFlow-capable switches enables exciting new network functionality, at the risk of programming errors that make communication less reliable. The centralized programming model, where a single controller program manages the network, seems ...

Elsevier Science Bv2015

Hardware/Software Approach for Code Synchronization in Low-Power Multi-Core Sensor Nodes

David Atienza Alonso, Giovanni Ansaloni, Ruben Braojos Lopez, Ivan Beretta

Latest embedded bio-signal analysis applications, targeting low-power Wireless Body Sensor Nodes (WBSNs), present conflicting requirements. On one hand, bio-signal analysis applications are continuously increasing their demand for high computing capabiliti ...

IEEE/ACM Press2014

DejaVu: Accelerating Resource Allocation in Virtualized Environments

Dejan Kostic, Nedeljko Vasic, Dejan Novakovic, Ricardo Bianchini

Effective resource management of virtualized environments is a challenging task. State-of-the-art management systems either rely on analytical models or evaluate resource allocations by running actual experiments. However, both approaches incur a significa ...

Acm Order Department, P O Box 64145, Baltimore, Md 21264 Usa2012

Performance Profiling of Virtual Machines

Willy Zwaenepoel, Jiaqing Du

Profilers based on hardware performance counters are indispensable for performance debugging of complex software systems. All modern processors feature hardware performance counters, but current virtual machine monitors (VMMs) do not properly expose them t ...

2011