Priyam Gupta

Hazel Torek, Long Tien Nguyen, Priyam Gupta et al.

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.

Priyam Gupta, Peter J. Schmid, Denis Sipp et al.

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.

Shreyam Gupta, P. Agrawal, Priyam Gupta

Temporal sequence modeling stands as the fundamental foundation for video prediction systems and real-time forecasting operations as well as anomaly detection applications. The achievement of accurate predictions through efficient resource consumption remains an ongoing issue in contemporary temporal sequence modeling. We introduce the Multi-Attention Unit (MAUCell) which combines Generative Adversarial Networks (GANs) and spatio-temporal attention mechanisms to improve video frame prediction capabilities. Our approach implements three types of attention models to capture intricate motion sequences. A dynamic combination of these attention outputs allows the model to reach both advanced decision accuracy along with superior quality while remaining computationally efficient. The integration of GAN elements makes generated frames appear more true to life therefore the framework creates output sequences which mimic real-world footage. The new design system maintains equilibrium between temporal continuity and spatial accuracy to deliver reliable video prediction. Through a comprehensive evaluation methodology which merged the perceptual LPIPS measurement together with classic tests MSE, MAE, SSIM and PSNR exhibited enhancing capabilities than contemporary approaches based on direct benchmark tests of Moving MNIST, KTH Action, and CASIA-B (Preprocessed) datasets. Our examination indicates that MAUCell shows promise for operational time requirements. The research findings demonstrate how GANs work best with attention mechanisms to create better applications for predicting video sequences.