Automated Reasoning
8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016, Proceedings
Page
%P
36 Result(s)
-
Chapter and Conference Paper
Output Range Analysis for Deep Feedforward Neural Networks
Given a neural network (NN) and a set of possible inputs to the network described by polyhedral constraints, we aim to compute a safe over-approximation of the set of possible output values. This operation is ...
-
Chapter and Conference Paper
TeLEx: Passive STL Learning Using Only Positive Examples
We propose a novel passive learning approach, TeLEx, to infer signal temporal logic formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. The approach requ...
-
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
Attacking the V: On the Resiliency of Adaptive-Horizon MPC
Inspired by the emerging problem of CPS security, we introduce the concept of controller-attacker games. A controller-attacker game is a two-player stochastic game, where the two players, a controller and an atta...
-
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...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Gamifying Program Analysis
Abstract interpretation is a powerful tool in program verification. Several commercial or industrial scale implementations of abstract interpretation have demonstrated that this approach can verify safety prop...
-
Chapter and Conference Paper
A Synthesized Algorithm for Interactive Consistency
We revisit the interactive consistency problem introduced by Pease, Shostak and Lamport. We first show that their algorithm does not achieve interactive consistency if faults are transient, even if faults are ...
-
Chapter and Conference Paper
Synthesis for Polynomial Lasso Programs
We present a method for the synthesis of polynomial lasso programs. These programs consist of a program stem, a set of transitions, and an exit condition, all in the form of algebraic assertions (conjunctions ...
-
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...
-
Article
Synthesizing switching logic using constraint solving
For a system that can operate in multiple different modes, we define the switching logic synthesis problem as follows: given a description of the dynamics in each mode of the system, find the conditions for sw...
-
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
Combining Equational Reasoning
Given a theory \(\mathbb{T}\) , a set of equations E, and a single equation e, the uniform word problem (UWP) is to dete...
-
Chapter and Conference Paper
Synthesizing Switching Logic Using Constraint Solving
A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we exte...
-
Chapter and Conference Paper
Invariant Checking for Programs with Procedure Calls
Invariants are a crucial component of the overall correctness of programs. We explore the theoretical limits for doing automatic invariant checking and show that invariant checking is decidable for a large cla...
-
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
Generating Box Invariants
Box invariant sets are box-shaped positively invariant sets. We show that box invariants are computable for a large class of nonlinear and hybrid systems. The technique for computing these invariants is based ...
-
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
Assertion Checking Unified
We revisit the connection between equality assertion checking in programs and unification that was recently described in [7]. Using a general formalization of this connection, we establish interesting connecti...
