13 Result(s)
within
Computer Science
Ashish Tiwari
-
Chapter and Conference Paper
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans
We introduce ARES, an efficient approximation algorithm for generating optimal plans (action sequences) that take an initial state of a Markov Decision Process (MDP) to a state whose cost is below a specified ...
-
Chapter and Conference Paper
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
We introduce a technique for component-based program synthesis that relies on searching for a target program and its proof of correctness simultaneously using a purely constraint-based approach, rather than ex...
-
Chapter and Conference Paper
Time-Aware Abstractions in HybridSal
HybridSal is a tool for enabling verification of hybrid systems using infinite bounded model checking and k-induction. The core component of the tool is an abstraction engine that automatically creates a discr...
-
Chapter and Conference Paper
A Nonlinear Real Arithmetic Fragment
We present a new procedure for testing satisfiability (over the reals) of a conjunction of polynomial equations. There are three possible return values for our procedure: it either returns a model for the input f...
-
Chapter and Conference Paper
HybridSAL Relational Abstracter
This paper describes the HybridSAL relational abstracter – a tool for verifying continuous and hybrid dynamical systems. The input to the tool is a model of a hybrid dynamical system and a safety property. The...
-
Chapter and Conference Paper
Timed Relational Abstractions for Sampled Data Control Systems
In this paper, we define timed relational abstractions for verifying sampled data control systems. Sampled data control systems consist of a plant, modeled as a hybrid system and a synchronous controller, mode...
-
Chapter and Conference Paper
Relational Abstractions for Continuous and Hybrid Systems
In this paper, we define relational abstractions of hybrid systems. A relational abstraction is obtained by replacing the continuous dynamics in each mode by a binary transition relation that relates a state o...
-
Chapter and Conference Paper
Constraint-Based Approach for Analysis of Hybrid Systems
This paper presents a constraint-based technique for discovering a rich class of inductive invariants (boolean combinations of polynomial inequalities of bounded degree) for verification of hybrid systems. The...
-
Chapter and Conference Paper
Computing Procedure Summaries for Interprocedural Analysis
We describe a new technique for computing procedure summaries for performing an interprocedural analysis on programs. Procedure summaries are computed by performing a backward analysis of procedures, but there...
-
Chapter and Conference Paper
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
We describe an abstract domain for representing useful invariants of heap-manipulating programs (in presence of recursive data structures and pointer arithmetic) written in languages like C or low-level code. ...
-
Chapter and Conference Paper
Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions
This paper presents results on the problem of checking equality assertions in programs whose expressions have been abstracted using combination of linear arithmetic and uninterpreted functions, and whose condi...
-
Chapter and Conference Paper
SAL 2
SAL (see http://sal.csl.sri.com) is an open suite of tools for analysis of state machines; it constitutes part of our vision for a Symbolic Analysis Laboratory that will eventually encompass SAL, the PVS verifica...
-
Chapter and Conference Paper
Termination of Linear Programs
We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is, a while loop with linear as...
