Dyck-reachability is a fundamental formulation for program analysis, which has been widely used to capture properly-matched-parenthesis program properties such as function calls/returns and field writes/reads. Bidirected Dyck-reachability is a relaxation of Dyck-reachability on bidirected graphs where each edge u → ( i v labeled by an open parenthesis “( i ” is accompanied with an inverse edge v → ) i u labeled by the corresponding close parenthesis “) i ”, and vice versa. In practice, many client analyses such as alias analysis adopt the bidirected Dyck-reachability formulation. Bidirected Dyck-reachability admits an optimal reachability algorithm. Specifically, given a graph with n nodes and m edges, the optimal bidirected Dyck-reachability algorithm computes all-pairs reachability information in O ( m ) time. This paper focuses on the dynamic version of bidirected Dyck-reachability. In particular, we consider the problem of maintaining all-pairs Dyck-reachability information in bidirected graphs under a sequence of edge insertions and deletions. Dynamic bidirected Dyck-reachability can formulate many program analysis problems in the presence of code changes. Unfortunately, solving dynamic graph reachability problems is challenging. For example, even for maintaining transitive closure, the fastest deterministic dynamic algorithm requires O ( n 2 ) update time to achieve O (1) query time. All-pairs Dyck-reachability is a generalization of transitive closure. Despite extensive research on incremental computation, there is no algorithmic development on dynamic graph algorithms for program analysis with worst-case guarantees. Our work fills the gap and proposes the first dynamic algorithm for Dyck reachability on bidirected graphs. Our dynamic algorithms can handle each graph update ( i.e. , edge insertion and deletion) in O ( n ·α( n )) time and support any all-pairs reachability query in O (1) time, where α( n ) is the inverse Ackermann function. We have implemented and evaluated our dynamic algorithm on an alias analysis and a context-sensitive data-dependence analysis for Java. We compare our dynamic algorithms against a straightforward approach based on the O ( m )-time optimal bidirected Dyck-reachability algorithm and a recent incremental Datalog solver. Experimental results show that our algorithm achieves orders of magnitude speedup over both approaches.
more »
« less
Interval-Based Parameter Identification for Structural Static Problems
We present an interval-based approach for parameter identification in
structural static problems. Our inverse formulation models uncertainties
in measurement data as interval and exploits the Interval Finite Element
Method (IFEM) combined with adjoint-based optimization. The inversion
consists of a two-step algorithm: first, an estimate of the parameters is
obtained by a deterministic iterative solver. Then, the algorithm switches
to the interval extension of the previous solver, using the deterministic estimate
of the parameters as an initial guess. The formulation is illustrated
in solutions of various numerical examples showing how the guaranteed
interval enclosures always contain Monte Carlo predictions.
more »
« less
- Award ID(s):
- 1634483
- NSF-PAR ID:
- 10181600
- Date Published:
- Journal Name:
- Reliable computing
- Volume:
- 23
- ISSN:
- 1573-1340
- Page Range / eLocation ID:
- 47-72
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
In this work, we introduce an interval formulation that accounts for uncertainty in supporting conditions of structural systems. Uncertainty in structural systems has been the focus of a wide range of research. Different models of uncertain parameters have been used. Conventional treatment of uncertainty involves probability theory, in which uncertain parameters are modeled as random variables. Due to specific limitation of probabilistic approaches, such as the need of a prior knowledge on the distributions, lack of complete information, and in addition to their intensive computational cost, the rationale behind their results is under debate. Alternative approaches such as fuzzy sets, evidence theory, and intervals have been developed. In this work, it is assumed that only bounds on uncertain parameters are available and intervals are used to model uncertainty. Here, we present a new approach to treat uncertainty in supporting conditions. Within the context of Interval Finite Element Method (IFEM), all uncertain parameters are modeled as intervals. However, supporting conditions are considered in idealized types and described by deterministic values without accounting for any form of uncertainty. In the current developed approach, uncertainty in supporting conditions is modeled as bounded range of values, i.e., interval value that capture any possible variation in supporting condition within a given interval. Extreme interval bounds can be obtained by analyzing the considered system under the conditions of the presence and absence of the specific supporting condition. A set of numerical examples is presented to illustrate and verify the accuracy of the proposed approach.more » « less
-
Graph Convolutional Network (GCN) has exhibited strong empirical performance in many real-world applications. The vast majority of existing works on GCN primarily focus on the accuracy while ignoring how confident or uncertain a GCN is with respect to its predictions. Despite being a cornerstone of trustworthy graph mining, uncertainty quantification on GCN has not been well studied and the scarce existing efforts either fail to provide deterministic quantification or have to change the training procedure of GCN by introducing additional parameters or architectures. In this paper, we propose the first frequentist-based approach named JuryGCN in quantifying the uncertainty of GCN, where the key idea is to quantify the uncertainty of a node as the width of confidence interval by a jackknife estimator. Moreover, we leverage the influence functions to estimate the change in GCN parameters without re-training to scale up the computation. The proposed JuryGCN is capable of quantifying uncertainty deterministically without modifying the GCN architecture or introducing additional parameters. We perform extensive experimental evaluation on real-world datasets in the tasks of both active learning and semi-supervised node classification, which demonstrate the efficacy of the proposed method.more » « less
-
Wireless systems must be resilient to jamming attacks. Existing mitigation methods based on multi-antenna processing require knowledge of the jammer's transmit characteristics that may be difficult to acquire, especially for smart jammers that evade mitigation by transmitting only at specific instants. We propose a novel method to mitigate smart jamming attacks on the massive multi-user multiple-input multiple-output (MU-MIMO) uplink which does not require the jammer to be active at any specific instant. By formulating an optimization problem that unifies jammer estimation and mitigation, channel estimation, and data detection, we exploit that a jammer cannot change its subspace within a coherence interval. Theoretical results for our problem formulation show that its solution is guaranteed to recover the users' data symbols under certain conditions. We develop two efficient iterative algorithms for approximately solving the proposed problem formulation: MAED, a parameter-free algorithm which uses forward-backward splitting with a box symbol prior, and SO-MAED, which replaces the prior of MAED with soft-output symbol estimates that exploit the discrete transmit constellation and which uses deep unfolding to optimize algorithm parameters. We use simulations to demonstrate that the proposed algorithms effectively mitigate a wide range of smart jammers without a priori knowledge about the attack type.more » « less
-
more » « less
Abstract We introduce the Weak-form Estimation of Nonlinear Dynamics (WENDy) method for estimating model parameters for non-linear systems of ODEs. Without relying on any numerical differential equation solvers, WENDy computes accurate estimates and is robust to large (biologically relevant) levels of measurement noise. For low dimensional systems with modest amounts of data, WENDy is competitive with conventional forward solver-based nonlinear least squares methods in terms of speed and accuracy. For both higher dimensional systems and stiff systems, WENDy is typically both faster (often by orders of magnitude) and more accurate than forward solver-based approaches. The core mathematical idea involves an efficient conversion of the strong form representation of a model to its weak form, and then solving a regression problem to perform parameter inference. The core statistical idea rests on the Errors-In-Variables framework, which necessitates the use of the iteratively reweighted least squares algorithm. Further improvements are obtained by using orthonormal test functions, created from a set of
$$C^{\infty }$$ https://github.com/MathBioCU/WENDy .
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- The DOI is not currently available.
