Rupak Majumdar

  1. Coordinate-invariant incremental Lyapunov functions.

    Authors: Majid Zamani, Rupak Majumdar
    Subjects: Optimization and Control
    Abstract

    The notion of incremental stability was proposed by several researchers as a
    strong property of dynamical and control systems. In this type of stability,
    the focus is on the convergence of trajectories with respect to themselves,
    rather than with respect to an equilibrium point or a particular trajectory.
    Similarly to stability, Lyapunov functions play an important role in the study
    of incremental stability.

  2. Algorithmic Verification of Asynchronous Programs.

    Authors: Rupak Majumdar, Pierre Ganty
    Subjects: Logic in Computer Science
    Abstract

    Asynchronous programming is a ubiquitous systems programming idiom to manage
    concurrent interactions with the environment. In this style, instead of waiting
    for time-consuming operations to complete, the programmer makes a non-blocking
    call to the operation and posts a callback task to a task buffer that is
    executed later when the time-consuming operation completes. A co-operative
    scheduler mediates the interaction by picking and executing callback tasks from
    the task buffer to completion (and these callbacks can post further callbacks
    to be executed later).

  3. Algorithms for Game Metrics.

    Authors: Krishnendu Chatterjee, Vishwanath Raman, Rupak Majumdar, Luca de Alfaro
    Subjects: Computer Science and Game Theory
    Abstract

    Simulation and bisimulation metrics for stochastic systems provide a
    quantitative generalization of the classical simulation and bisimulation
    relations. These metrics capture the similarity of states with respect to
    quantitative specifications written in the quantitative {\mu}-calculus and
    related probabilistic logics. We first show that the metrics provide a bound
    for the difference in long-run average and discounted average behavior across
    states, indicating that the metrics can be used both in system verification,
    and in performance evaluation.

  4. Refinement type inference via abstract interpretation.

    Authors: Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
    Subjects: Programming Languages
    Abstract

    Refinement Types are a promising approach for checking behavioral properties
    of programs written using advanced language features like higher-order
    functions, parametric polymorphism and recursive datatypes. The main limitation
    of refinement type systems to date is the requirement that the programmer
    provides the types of all functions, after which the type system can check the
    types and hence, verify the program. In this paper, we show how to
    automatically infer refinement types, using existing abstract interpretation
    tools for imperative programs.

Syndicate content