6 papers
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…
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…
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…
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…