Publications associées à Bounds checking

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

Homothetic Tube Model Predictive Control With Multi-Step Predictors

Giancarlo Ferrari Trecate, Danilo Saccani, Melanie Nicole Zeilinger

We present a robust model predictive control (MPC) framework for linear systems facing bounded parametric uncertainty and bounded disturbances. Our approach deviates from standard MPC formulations by integrating multi-step predictors, which provide reduced ...

Ieee-Inst Electrical Electronics Engineers Inc2023

Admissibility of Uncertain Injections in Quadratic Algebraic Systems

Jean-Yves Le Boudec, Cong Wang, Eleni Stai

We study the admissibility problem in multivariate algebraic systems, such as ac electrical networks, where the power injection is quadratic in the state. The goal of such systems is to ensure that the state stays in some security set (e.g., magnitudes of ...

2021

RetroWrite: Statically Instrumenting COTS Binaries for Fuzzing and Sanitization

Mathias Josef Payer, Duo Xu

Analyzing the security of closed source binaries is currently impractical for end-users, or even developers who rely on third-party libraries. Such analysis relies on automatic vulnerability discovery techniques, most notably fuzzing with sanitizers enable ...

IEEE COMPUTER SOC2020

Forbidden induced subposets of given height

Istvan Tomon

Let P be a partially ordered set. The function La* (n, P) denotes the size of the largest family F subset of 2([n]) that does not contain an induced copy of P. It was proved by Methuku and Palvolgyi that there exists a constant C-P (depending only on P) su ...

ACADEMIC PRESS INC ELSEVIER SCIENCE2019

Low-rank tensor methods for large Markov chains and forward feature selection methods

Francisco Santos Paredes Quartin de Macedo

In the first part of this thesis, we present and compare several approaches for the determination of the steady-state of large-scale Markov chains with an underlying low-rank tensor structure. Such structure is, in our context of interest, associated with ...

EPFL2018

On verifying causal consistency

Rachid Guerraoui, Jad Hamza

Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automaticall ...

Algorithmic Resource Verification

Ravichandhran Kandhadai Madhavan

Static estimation of resource utilisation of programs is a challenging and important problem with numerous applications. In this thesis, I present new algorithms that enable users to specify and verify their desired bounds on resource usage of functional p ...

EPFL2017

Contract-Based Resource Verification for Higher-Order Functions with Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...

Assoc Computing Machinery2017

SMT-Based Checking of Predicate-Qualified Types for Scala

Viktor Kuncak, Georg Stefan Schmid

We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in ...

Assoc Computing Machinery2016