DCMay 26
A Formal Semantics of C with OpenMP ParallelismKe Du, Anshu Sharma, Liyi Li et al.
OpenMP is a popular parallelization framework that lets users transform sequential code into parallel code with a few simple annotations. Unfortunately, it is also easy to inadvertently introduce errors by adding OpenMP pragmas into otherwise correct programs, including both logic errors and race conditions. We present a formal semantics for C code with OpenMP directives, building on the C semantics of the CompCert verified compiler and its extension to concurrency. Our semantics captures subtle interactions between OpenMP directives and variable state that have been obscured by previous OpenMP semantics, and provides a basis for detecting undesired behaviors introduced by incorrect annotations: in particular, any successful execution is guaranteed to be free of data races.
LGNov 16, 2022
Dwelling Type Classification for Disaster Risk Assessment Using Satellite ImageryMd Nasir, Tina Sederholm, Anshu Sharma et al.
Vulnerability and risk assessment of neighborhoods is essential for effective disaster preparedness. Existing traditional systems, due to dependency on time-consuming and cost-intensive field surveying, do not provide a scalable way to decipher warnings and assess the precise extent of the risk at a hyper-local level. In this work, machine learning was used to automate the process of identifying dwellings and their type to build a potentially more effective disaster vulnerability assessment system. First, satellite imageries of low-income settlements and vulnerable areas in India were used to identify 7 different dwelling types. Specifically, we formulated the dwelling type classification as a semantic segmentation task and trained a U-net based neural network model, namely TernausNet, with the data we collected. Then a risk score assessment model was employed, using the determined dwelling type along with an inundation model of the regions. The entire pipeline was deployed to multiple locations prior to natural hazards in India in 2020. Post hoc ground-truth data from those regions was collected to validate the efficacy of this model which showed promising performance. This work can aid disaster response organizations and communities at risk by providing household-level risk information that can inform preemptive actions.
CEApr 13
A Physics-Aware Variational Graph Autoencoder for Joint Modal Identification with Uncertainty QuantificationBhargav Nath, Mehulkumar Lakhadive, Anshu Sharma et al.
Reliable modal identification from output-only vibration data remains a challenging problem under measurement noise, sparse sensing, and structural variability. These challenges intensify when global modal quantities and spatially distributed mode shapes must be estimated jointly from frequency-domain data. This work presents a physics-aware variational graph autoencoder, termed UResVGAE, for joint modal identification with uncertainty quantification from power spectral density (PSD) representations of truss structures. The framework represents each structure as a graph in which node attributes encode PSD and geometric information, while edges capture structural connectivity. A residual GraphSAGE-based encoder, attention-driven graph pooling, and a variational latent representation are combined to learn both graph-level and node-level modal information within a single, unified formulation. Natural frequencies and damping ratios are predicted through evidential regression, and full-field mode shapes are reconstructed through a dedicated node-level decoder that fuses global latent information with local graph features. Physical consistency is promoted via mode-shape reconstruction and orthogonality regularisation. The framework is assessed on numerically generated truss populations under varying signal-to-noise ratios and sensor availability. Results demonstrate accurate prediction of natural frequencies, damping ratios, and mode shapes, with high modal assurance criterion values and stable performance under noisy and sparse sensing conditions. Reliability analysis indicates that the predictive uncertainty is broadly consistent with empirical coverage. The proposed framework offers a coherent and physically grounded graph-based route for joint modal identification with calibrated uncertainty from frequency-domain structural response data.