Position:  PhD Candidate

Current Institution:  Rice University

Abstract:  Scalable Quantitative Verification and its Applications

On the one hand our increasing dependence on computerized systems emphasizes on the importance of systems correctness; On the other hand their increasing complexity makes correctness harder to achieve. The formal reasoning about complex quantitative properties of these systems such as cost reward runtime and the like oers automated techniques to ensure system correctness. Unsurprisingly, it has real-world applications in verification of decentralized cryptocurrency protocols network-trac monitoring optimal-cost motion-planning in robotics and more. So far, however, the formal reasoning of quantitative properties has been addressed only from a theoretical point of view and not with practical considerations. The goal of my dissertation is to develop new techniques to bridge the gap between theory and practice of quantitative reasoning to harness its untapped potential in real-world applications. At the core of reasoning about quantitative properties of systems lies the fundamental problem of comparison of the quantities associated with system runs. In my research, I have developed an automata-theoretic technique for the comparison of quantities of system runs and have utilized it to provide the rst and, to the best of our knowledge, only automatically-generated proof as opposed to a manually-generated proof of the non-incentive compatibility of the Bitcoin protocol. I have also applied my automata-theoretic comparison technique in quantitative model-checking to design resource-efficient systems and to establish new theoretical complexity bounds specifically the PSPACE-completeness of discounted-sum inclusion with integer discount-factors.

Bio:
Suguman Bansal is a PhD candidate in the Department of Computer Science at Rice University. Her research interests spans formal methods, specifically the application of quantitative verification and reactive synthesis to real-time decision making in multi-agent systems. She received the Andrew Ladd Fellowship and Gold Medal at the Association for Computing Machinery (ACM) Student Research Competition at POPL 2016. She was also a visiting graduate student at the Simons Institute Spring Program on “Real-Time Decision Making” at the University of California, Berkeley, in 2018. She spent the summers of 2017 and 2018 interning at Nokia Bell Labs.