Publications related to Formalizing and verifying transactional memories

Oligolithic Cross-task Optimizations across Isolated Workloads

Anastasia Ailamaki, Eleni Zapridou, Panagiotis Sioulas

Enterprises collect data in large volumes and leverage them to drive numerous concurrent decisions and business processes. Their teams deploy multiple applications that often operate concurrently on the same data and infrastructure but have widely differen ...

2024

Driving and suppressing the human language network using large language models

Martin Schrimpf

Transformer models such as GPT generate human-like language and are predictive of human brain responses to language. Here, using functional-MRI-measured brain responses to 1,000 diverse sentences, we first show that a GPT-based encoding model can predict t ...

Nature Portfolio2024

Formal Foundations of Capture Tracking

Aleksander Slawomir Boruch-Gruszecki

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...

EPFL2024

Secure Interface Design Leveraging Hardware/Software Support

Atri Bhattacharyya

Computer systems rely heavily on abstraction to manage the exponential growth of complexity across hardware and software. Due to practical considerations of compatibility between components of these complex systems across generations, developers have favou ...

EPFL2024

The conceptual foundations of innate immunity: Taking stock 30 years later

Bruno Lemaitre

While largely neglected over decades during which adaptive immunity captured most of the attention, innate immune mechanisms have now become central to our understanding of immunology. Innate immunity provides the first barrier to infection in vertebrates, ...

2024

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

EdgeAI-Aware Design of In-Memory Computing Architectures

Marco Antonio Rios

Driven by the demand for real-time processing and the need to minimize latency in AI algorithms, edge computing has experienced remarkable progress. Decision-making AI applications stand out for their heavy reliance on data-centric operations, predominantl ...

EPFL2024

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Yichen Xu, Aleksander Slawomir Boruch-Gruszecki

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

One-shot Garbage Collection for In-memory OLTP through Temporality-aware Version Storage

Anastasia Ailamaki, Syed Mohammad Aunn Raza, Periklis Chrysogelos, Angelos Christos Anadiotis

Most modern in-memory online transaction processing (OLTP) engines rely on multi-version concurrency control (MVCC) to provide data consistency guarantees in the presence of conflicting data accesses. MVCC improves concurrency by generating a new version o ...

ACM2023