![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
Chapter and Conference Paper
Neural Flocking: MPC-Based Supervised Learning of Flocking Controllers
We show how a symmetric and fully distributed flocking controller can be synthesized using Deep Learning from a centralized flocking controller. Our approach is based on Supervised Learning, with the centralized ...
-
Chapter
Bioinformatics Applications in Advancing Animal Virus Research
Viruses serve as infectious agents for all living entities. There have been various research groups that focus on understanding the viruses in terms of their host-viral relationships, pathogenesis and immune e...
-
Article
Tetralogy of Fallot with Restrictive Ventricular Septal Defect
-
Article
Open AccessCurcumin encapsulated zeolitic imidazolate frameworks as stimuli responsive drug delivery system and their interaction with biomimetic environment
Metal organic frameworks (MOFs) exhibit unique features of finely tunable pore structures, excellent chemical stability and flexible surface structural functionality, making them advantageous for a wide range ...
-
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...
-
Article
Open AccessComputing minimal nutrient sets from metabolic networks via linear constraint solving
As more complete genome sequences become available, bioinformatics challenges arise in how to exploit genome sequences to make phenotypic predictions. One type of phenotypic prediction is to determine sets of ...
-
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
Erratum: Analyzing a Discrete Model of Aplysia Central Pattern Generator
We present a discrete formal model of the central pattern generator (CPG) located in the buccal ganglia of Aplysia that is responsible for mediating the rhythmic movements of its foregut during feeding. Our start...
-
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...