This paper investigates ER(r^Z), that is the extension of the existential theory of the reals by an additional unary predicate r^Z for the integer powers of a fixed computable real number r > 0. If all we have access to is a Turing machine computing r, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when:

1. r is known to be transcendental, or
2. r is a root of some given integer polynomial (that is, r is algebraic). In other words, knowing the algebraicity of r suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that r enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of ER(r^Z) is
3. in EXPSPACE if r is an algebraic number, and
4. in 3EXP if r is a logarithm of an algebraic number, Euler’s e, or the number pi, among others. To establish our results, we first observe that the satisfiability problem of ER(r^Z) reduces in exponential time to the problem of solving quantifier-free instances of the theory of the reals where variables range over r^Z. We then prove that these instances have a small witness property: only finitely many integer powers of r must be considered to find whether a formula is satisfiable. Our complexity results are shown by relying on well-established machinery from Diophantine approximation and transcendental number theory, such as bounds for the transcendence measure of numbers. As a by-product of our results, we are able to remove the appeal to Schanuel’s conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler’s e and the aversion factor is a fixed algebraic number, the problem is (unconditionally) in EXP.

With the increasing popularity of blockchains, cryptocurrencies are now accepted for the purchase of digital goods, such as e-books or gift cards. A contingent payment is a cryptographic protocol that models digital purchases, and it involves a buyer and a seller. The buyer owns crypto-coins, and the seller owns a digital product. Contingent payment ensures that the buyer and the seller can exchange coins and product securely. However, observers of the blockchain might learn which buyer purchased from which seller based on the information contained in the transaction. Is it possible to extend contingent payment so that the relationship between buyer and seller is hidden? In this talk, I will present how contingent payment works, as well as coin mixing, practical technique to hide the relationship between a sender and a receiver in a transaction regardless of the blockchain. Then, I will show that existing coin mixing schemes cannot be applied to contingent payment as they lead to devastating attacks. My presentation ends with MixBuy, the first protocol that hides the relationship between buyer and seller in a contingent payment, regardless of the blockchain. This talk is related to the paper: https://eprint.iacr.org/2024/953, which will be presented at The 25th Privacy Enhancing Technologies Symposium in 2025.

The massive scale and heterogeneity of current workloads and platforms, such as cloud applications and large machine learning models, break the effectiveness of conventional resource management approaches and create the need for new, custom-tailored systems solutions. The use of machine learning methods can enable robust management decisions, but comes with substantial overheads, practicality and interpretability concerns, therefore it is crucial to enable its practical use. In this talk, I will demonstrate data-driven insights and observations that enable the use of lightweight prediction models for forecasting resource usage and improving upon cloud resource efficiency. In addition, I will describe missed opportunities in the efficient serving of Large Language Model (LLM) inference. Finally, I will conclude with my research vision on the upcoming challenges and directions in system-level resource management.

Cryptography plays a prominent role in today’s increasingly digital society. In fact, virtually all existing systems rely on cryptography at their core. Therefore, it is utterly important to build and analyze cryptographic protocols to secure real world systems. In this talk, I will share my vision for establishing secure and privacy-preserving blockchain applications through cryptographic protocols by showcasing examples of my work in the field. As an example, I will present our research on adaptor signatures, a novel cryptographic scheme that binds the creation of a digital signature to the knowledge of a cryptographic secret other than the signing key. In the realm of blockchain-based systems, the adaptor signatures scheme has become the building block for many blockchain applications proposed so far. Finally, I will conclude by highlighting my ongoing research efforts and future research directions.

Robust forecasts of future resource usage in cloud computing environments enable high efficiency in resource management solutions, such as autoscaling and overcommitment policies. Production-level systems use lightweight combinations of historical information to enable practical deployments. Recently, Machine Learning (ML) models, in particular Long Short Term Memory (LSTM) neural networks, have been proposed by various works, for their improved predictive capabilities. Following this trend, we train LSTM models and observe high levels of prediction accuracy, even on unseen data. Upon meticulous visual inspection of the results, we notice that although the predicted values seem highly accurate, they are nothing but versions of the original data shifted by one time step into the future. Yet, this clear shift seems to be enough to produce a robust forecast, because the values are highly correlated across time. We investigate time series data of various resource usage metrics (CPU, memory, network, disk I/O) across different cloud providers and levels, such as at the physical or virtual machine-level and at the application job-level. We observe that resource utilisation displays very small variations in consecutive time steps. This insight can enable very simple solutions, such as data shifts, to be used for cloud resource forecasting and deliver highly accurate predictions. This is the reason why we ask whether complex machine learning models are even necessary to use. We envision that practical resource management systems need to first identify the extent to which simple solutions can be effective, and resort to using machine learning to the extent that enables its practical use. This talk will be based on work that has been presented in the 14th edition of the annual ACM Symposium on Cloud Computing (SoCC ‘23).