arXiv subjects

Priyam Gupta

Publications and source records attributed to Priyam Gupta.

6 recordsLinked to original sources

arXiv2026

Drone-Assisted UAV-UGV Collaboration for Autonomous Navigation in Snow-Covered Terrain

This paper presents a collaborative UAV-UGV navigation framework for high-altitude, snow-covered terrain, where reduced visibility and unstable ground render conventional methods ineffective. We introduce a custom efficient U-Net architecture that falls under the computational constraints for real-time road segmentation, utilizing a novel synthetic snow data augmentation technique to achieve 96.5% segmentation accuracy. For UAV localization, we implement an Extended Kalman Filter (EKF) fusing onboard GPS and IMU data, achieving a maximum observed positional error of +-0.5 meters. The UGV position is determined via a visual tracking pipeline using YOLOv5 and depth data from the UAV's RGB-D camera. A dynamic path planning algorithm utilizes this segmentation to adjust for snow drifts, enabling successful navigation in obscured test environment with minimal deviation.

cs.RO↗

arXiv2026

Gradually Verifying Unfolding Expressions & Pure Functions

Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent functions that can be used in specifications, are used in deductive program verifiers based on implicit dynamic frames, such as Gradual C0, Gobra, Nagini, and SnaKt, to increase the modularity of specifications involving ownership. In this paper, we present the formal semantics for unfolding expressions and pure functions for a static verifier using symbolic execution, extend it for a gradual verifier, and provide a proof of soundness. To support Gradual C0, our proof is in the setting of gradual verification, a deductive program verification system that combines static and dynamic verification to allow partial specifications. However, because the gradual verifier is a conservative extension of a static verifier, our results also apply to static verifiers that use symbolic execution, such as the Silicon symbolic execution backend for the Viper verification infrastructure used by Gobra, Nagini, and SnaKt.

cs.PL↗

arXiv2025

Increasing the Expressiveness of a Gradual Verifier

Static verification provides strong correctness guarantees for code; however, fully specifying programs for static verification is a complex, burdensome process for users. Gradual verification was introduced to make this process easier by supporting the verification of partially specified programs. The only currently working gradual verifier, Gradual C0, successfully verifies heap manipulating programs, but lacks expressiveness in its specification language. This paper describes the design and implementation of an extension to Gradual C0 that supports unfolding expressions, which allow more intuitive specifications of recursive heap data structures.

cs.PL↗

arXiv2025

Resolving Spatio-Temporal Entanglement in Video Prediction via Multi-Modal Attention

The fast progress in computer vision has necessitated more advanced methods for temporal sequence modeling. This area is essential for the operation of autonomous systems, real-time surveillance, and predicting anomalies. As the demand for accurate video prediction increases, the limitations of traditional deterministic models, particularly their struggle to maintain long-term temporal coherence while providing high-frequency spatial detail, have become very clear. This report provides an exhaustive analysis of the Multi-Attention Unit Cell (MAUCell), a novel architectural framework that represents a significant leap forward in video frame prediction. By synergizing Generative Adversarial Networks (GANs) with a hierarchical "STAR-GAN" processing strategy and a triad of specialized attention mechanisms (Temporal, Spatial, and Pixel-wise), the MAUCell addresses the persistent "deep-in-time" dilemma that plagues Recurrent Neural Networks (RNNs). Our analysis shows that the MAUCell framework successfully establishes a new state-of-the-art benchmark, especially in its ability to produce realistic video sequences that closely resemble real-world footage while ensuring efficient inference for real-time deployment. Through rigorous evaluation on datasets: Moving MNIST, KTH Action, and CASIA-B, the framework shows superior performance metrics, especially in Learned Perceptual Image Patch Similarity (LPIPS) and Structural Similarity Index (SSIM). This success confirms its dual-pathway information transformation system. This report details the theoretical foundations, detailed structure and broader significance of MAUCell, presenting it as a valuable solution for video forecasting tasks that require high precision and limited resources.

cs.CV↗

arXiv2023

Mori-Zwanzig latent space Koopman closure for nonlinear autoencoder

The Koopman operator presents an attractive approach to achieve global linearization of nonlinear systems, making it a valuable method for simplifying the understanding of complex dynamics. While data-driven methodologies have exhibited promise in approximating finite Koopman operators, they grapple with various challenges, such as the judicious selection of observables, dimensionality reduction, and the ability to predict complex system behaviours accurately. This study presents a novel approach termed Mori-Zwanzig autoencoder (MZ-AE) to robustly approximate the Koopman operator in low-dimensional spaces. The proposed method leverages a nonlinear autoencoder to extract key observables for approximating a finite invariant Koopman subspace and integrates a non-Markovian correction mechanism using the Mori-Zwanzig formalism. Consequently, this approach yields an approximate closure of the dynamics within the latent manifold of the nonlinear autoencoder, thereby enhancing the accuracy and stability of the Koopman operator approximation. Demonstrations showcase the technique's improved predictive capability for flow around a cylinder. It also provides a low dimensional approximation for Kuramoto-Sivashinsky (KS) with promising short-term predictability and robust long-term statistical performance. By bridging the gap between data-driven techniques and the mathematical foundations of Koopman theory, MZ-AE offers a promising avenue for improved understanding and prediction of complex nonlinear dynamics.

cs.LG↗

arXiv2021

Metaheuristic Optimization Framework for Drag Reduction Using Bioinspired Surface Riblets

Emulating natural mechanisms in technology has become a very efficient technique to optimize and improve the current machinery. Riblets are such kinds of bio-inspired surface patterns which are seen on Sharks. Their geometric properties induce secondary flows resulting in lower drag, allowing Sharks to achieve such high speeds. Secondary flows are broadly subcategorized into Prandtls first and second kind; the secondary flows induced by riblets belong primarily to Prandtls second kind. These secondary flows have been proven to delay the boundary layer separation by reducing momentum losses. This paper aims to optimize the use of these bio-inspired patterns on an airfoil. By applying the ribletted surface on an airfoil, the boundary layer separation can be delayed, thus leading to a reduction in drag and increasing the critical angle of attack. Specific geometric properties such as the height and the wavelength of the riblets are varied to find the most optimal design. The design framework couples the optimization algorithm, computational fluid dynamics, and post-processing analysis. An Invasive Weed Model is implemented for optimization due to its commendable performance in converging close to global optima. The optimization process is initialized by generating a population of riblet profiles with randomly distributed geometry parameters. These profiles are then evolved over generations with the objective to minimize the drag, which is computed through Computational Fluid Dynamics simulations conducted on OpenFOAM. The optimized geometries show a significant reduction in drag as compared to bare airfoils. Lastly, a flow field analysis of the optimized geometry established using the genetic algorithm is done to understand the riblets-induced enhancement in the aerodynamic efficiency of the airfoil.

physics.flu-dyn↗