15 citations · 66 across the 23 of their papers we have counts for
13 papers · 1 filter
Parameterized Algorithms and Complexity for Function Merging with Branch Reordering
Amir K. Goharshady, Kerim Kochekov, Tian Shu +1
Binary size reduction is an increasingly important optimization objective for compilers. One emerging technique is function merging, where multiple similar functions are merged int…
Series-Parallel-Loop Decompositions of Control-flow Graphs
Xuran Cai, Amir Goharshady, S Hitarth +1
Control-flow graphs (CFGs) of structured programs are well known to exhibit strong sparsity properties. Traditionally, this sparsity has been modeled using graph parameters such as…
Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady +2
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witne…
Template-based Program Synthesis using Stellensätze
Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi +1
Template-based synthesis, also known as sketching, is a localized approach to program synthesis in which the programmer provides not only a specification, but also a high-level ``s…
Quantitative Analysis of Assertion Violations in Probabilistic Programs
Jinyi Wang, Yican Sun, Hongfei Fu +2
In this work, we consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide autom…
Concentration-Bound Analysis for Probabilistic Programs and Probabilistic Recurrence Relations
Jinyi Wang, Yican Sun, Hongfei Fu +3
Analyzing probabilistic programs and randomized algorithms are classical problems in computer science. The first basic problem in the analysis of stochastic processes is to conside…
Inductive Reachability Witnesses
Ali Asadi, Krishnendu Chatterjee, Hongfei Fu +2
In this work, we consider the fundamental problem of reachability analysis over imperative programs with real variables. The reachability property requires that a program can reach…
Cost Analysis of Nondeterministic Probabilistic Programs
Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady +3
We consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. P…
Computational Approaches for Stochastic Shortest Path on Succinct MDPs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady +1
We consider the stochastic shortest path (SSP) problem for succinct Markov decision processes (MDPs), where the MDP consists of a set of variables, and a set of nondeterministic ru…
Quantitative Analysis of Smart Contracts
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Yaron Velner
Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and t…
Non-polynomial Worst-Case Analysis of Recursive Programs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady
We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving…
Termination Analysis of Probabilistic Programs through Positivstellensatz's
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady
We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic…
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen +1
We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations…