9 papers
Pushdown Model Checking Above the Cubic Bottleneck
A. R. Balasubramanian, Dmitry Chistikov, Rupak Majumdar
Many problems in the verification of recursive programs can be reduced to pushdown model checking. In this problem, we are given as input a pushdown automaton (PDA) over a constant…
Reachability in Fixed-Dimensional Continuous VASS
Michal Ajdarów, A. R. Balasubramanian, Łukasz Orlikowski
Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It…
Hypersequent Calculi Have Ackermannian Complexity
A. R. Balasubramanian, Vitor Greati, Revantha Ramanayake
For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on (Dickson's lemma), yi…
Reasoning Distillation for Lightweight Automated Program Repair
Aanand Balasubramanian, Sashank Silwal
We study whether lightweight symbolic reasoning supervision can improve fix type classification in compact automated program repair models. Small code models are attractive for res…
State Space Estimation for DPOR-based Model Checkers(Extended Version)
A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar +2
We study the estimation problem for concurrent programs: given a bounded program , estimate the number of Mazurkiewicz trace-equivalence classes induced by its interleavings. Th…
General Decidability Results for Systems with Continuous Counters
A. R. Balasubramanian, Matthew Hague, Rupak Majumdar +2
Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs.…
Presburger Functional Synthesis: Complexity and Tractable Normal Forms
S. Akshay, A. R. Balasubramanian, Supratik Chakraborty +1
Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs…
Decidability and Complexity of Decision Problems for Affine Continuous VASS
A. R. Balasubramanian
Vector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which c…
Reachability in Continuous Pushdown VASS
A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam +1
Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but n…