Showing 1–26 of 26 results for author: K, G

Enhanced Tuberculosis Bacilli Detection using Attention-Residual U-Net and Ensemble Classification

Authors: Greeshma K, Vishnukumar S

Abstract: Tuberculosis (TB), caused by Mycobacterium tuberculosis, remains a critical global health issue, necessitating timely diagnosis and treatment. Current methods for detecting tuberculosis bacilli from bright field microscopic sputum smear images suffer from low automation, inadequate segmentation performance, and limited classification accuracy. This paper proposes an efficient hybrid approach that… ▽ More Tuberculosis (TB), caused by Mycobacterium tuberculosis, remains a critical global health issue, necessitating timely diagnosis and treatment. Current methods for detecting tuberculosis bacilli from bright field microscopic sputum smear images suffer from low automation, inadequate segmentation performance, and limited classification accuracy. This paper proposes an efficient hybrid approach that combines deep learning for segmentation and an ensemble model for classification. An enhanced U-Net model incorporating attention blocks and residual connections is introduced to precisely segment microscopic sputum smear images, facilitating the extraction of Regions of Interest (ROIs). These ROIs are subsequently classified using an ensemble classifier comprising Support Vector Machine (SVM), Random Forest, and Extreme Gradient Boost (XGBoost), resulting in an accurate identification of bacilli within the images. Experiments conducted on a newly created dataset, along with public datasets, demonstrate that the proposed model achieves superior segmentation performance, higher classification accuracy, and enhanced automation compared to existing methods. △ Less

Submitted 7 January, 2025; originally announced January 2025.

Efficient and Accurate Tuberculosis Diagnosis: Attention Residual U-Net and Vision Transformer Based Detection Framework

Authors: Greeshma K, Vishnukumar S

Abstract: Tuberculosis (TB), an infectious disease caused by Mycobacterium tuberculosis, continues to be a major global health threat despite being preventable and curable. This burden is particularly high in low and middle income countries. Microscopy remains essential for diagnosing TB by enabling direct visualization of Mycobacterium tuberculosis in sputum smear samples, offering a cost effective approac… ▽ More Tuberculosis (TB), an infectious disease caused by Mycobacterium tuberculosis, continues to be a major global health threat despite being preventable and curable. This burden is particularly high in low and middle income countries. Microscopy remains essential for diagnosing TB by enabling direct visualization of Mycobacterium tuberculosis in sputum smear samples, offering a cost effective approach for early detection and effective treatment. Given the labour-intensive nature of microscopy, automating the detection of bacilli in microscopic images is crucial to improve both the expediency and reliability of TB diagnosis. The current methodologies for detecting tuberculosis bacilli in bright field microscopic sputum smear images are hindered by limited automation capabilities, inconsistent segmentation quality, and constrained classification precision. This paper proposes a twostage deep learning methodology for tuberculosis bacilli detection, comprising bacilli segmentation followed by classification. In the initial phase, an advanced U-Net model employing attention blocks and residual connections is proposed to segment microscopic sputum smear images, enabling the extraction of Regions of Interest (ROIs). The extracted ROIs are then classified using a Vision Transformer, which we specifically customized as TBViT to enhance the precise detection of bacilli within the images. For the experiments, a newly developed dataset of microscopic sputum smear images derived from Ziehl-Neelsen-stained slides is used in conjunction with existing public datasets. The qualitative and quantitative evaluation of the experiments using various metrics demonstrates that the proposed model achieves significantly improved segmentation performance, higher classification accuracy, and a greater level of automation, surpassing existing methods. △ Less

Submitted 7 January, 2025; originally announced January 2025.

Farmer.Chat: Scaling AI-Powered Agricultural Services for Smallholder Farmers

Authors: Namita Singh, Jacqueline Wang'ombe, Nereah Okanga, Tetyana Zelenska, Jona Repishti, Jayasankar G K, Sanjeev Mishra, Rajsekar Manokaran, Vineet Singh, Mohammed Irfan Rafiq, Rikin Gandhi, Akshay Nambi

Abstract: Small and medium-sized agricultural holders face challenges like limited access to localized, timely information, impacting productivity and sustainability. Traditional extension services, which rely on in-person agents, struggle with scalability and timely delivery, especially in remote areas. We introduce FarmerChat, a generative AI-powered chatbot designed to address these issues. Leveraging Ge… ▽ More Small and medium-sized agricultural holders face challenges like limited access to localized, timely information, impacting productivity and sustainability. Traditional extension services, which rely on in-person agents, struggle with scalability and timely delivery, especially in remote areas. We introduce FarmerChat, a generative AI-powered chatbot designed to address these issues. Leveraging Generative AI, FarmerChat offers personalized, reliable, and contextually relevant advice, overcoming limitations of previous chatbots in deterministic dialogue flows, language support, and unstructured data processing. Deployed in four countries, FarmerChat has engaged over 15,000 farmers and answered over 300,000 queries. This paper highlights how FarmerChat's innovative use of GenAI enhances agricultural service scalability and effectiveness. Our evaluation, combining quantitative analysis and qualitative insights, highlights FarmerChat's effectiveness in improving farming practices, enhancing trust, response quality, and user engagement. △ Less

Submitted 8 October, 2024; v1 submitted 13 September, 2024; originally announced September 2024.

Comments: 35 pages

Delay Balancing with Clock-Follow-Data: Optimizing Area Delay Trade-offs for Robust Rapid Single Flux Quantum Circuits

Authors: Robert S. Aviles, Phalgun G K, Peter A. Beerel

Abstract: This paper proposes an algorithm for synthesis of clock-follow-data designs that provides robustness against timing violations for RSFQ circuits while maintaining high performance and minimizing area costs. Since superconducting logic gates must be clocked, managing data flow is a challenging problem that often requires the insertion of many path balancing D Flips (DFFs) to properly sequence data,… ▽ More This paper proposes an algorithm for synthesis of clock-follow-data designs that provides robustness against timing violations for RSFQ circuits while maintaining high performance and minimizing area costs. Since superconducting logic gates must be clocked, managing data flow is a challenging problem that often requires the insertion of many path balancing D Flips (DFFs) to properly sequence data, leading to a substantial increase in area. To address this challenge, we present an algorithm to insert DFFs into clock-follow-data RSFQ circuits that partially balances the delays within the circuit to achieve a target throughput while minimizing area. Our algorithm can account for expected timing variations and, by adjusting the bias of the clock network and clock frequency, we can mitigate unexpected timing violations post-fabrication. Quantifying the benefits of our approach with a benchmark suite with nominal delays, our designs offer an average 1.48x improvement in area delay product (ADP) over high frequency full path balancing (FPB) designs and a 2.07x improvement in ADP over the state of the art robust circuits provided by state-of-the-art (SOTA) multi-phase clocking solutions. △ Less

Submitted 7 September, 2024; originally announced September 2024.

Improving Retrieval in Sponsored Search by Leveraging Query Context Signals

Authors: Akash Kumar Mohankumar, Gururaj K, Gagan Madan, Amit Singh

Abstract: Accurately retrieving relevant bid keywords for user queries is critical in Sponsored Search but remains challenging, particularly for short, ambiguous queries. Existing dense and generative retrieval models often fail to capture nuanced user intent in these cases. To address this, we propose an approach to enhance query understanding by augmenting queries with rich contextual signals derived from… ▽ More Accurately retrieving relevant bid keywords for user queries is critical in Sponsored Search but remains challenging, particularly for short, ambiguous queries. Existing dense and generative retrieval models often fail to capture nuanced user intent in these cases. To address this, we propose an approach to enhance query understanding by augmenting queries with rich contextual signals derived from web search results and large language models, stored in an online cache. Specifically, we use web search titles and snippets to ground queries in real-world information and utilize GPT-4 to generate query rewrites and explanations that clarify user intent. These signals are efficiently integrated through a Fusion-in-Decoder based Unity architecture, enabling both dense and generative retrieval with serving costs on par with traditional context-free models. To address scenarios where context is unavailable in the cache, we introduce context glancing, a curriculum learning strategy that improves model robustness and performance even without contextual signals during inference. Extensive offline experiments demonstrate that our context-aware approach substantially outperforms context-free models. Furthermore, online A/B testing on a prominent search engine across 160+ countries shows significant improvements in user engagement and revenue. △ Less

Submitted 18 October, 2024; v1 submitted 19 July, 2024; originally announced July 2024.

Comments: Accepted to EMNLP 2024 Industry Track. 10 pages, 10 tables, 1 figure

UniDEC : Unified Dual Encoder and Classifier Training for Extreme Multi-Label Classification

Authors: Siddhant Kharbanda, Devaansh Gupta, Gururaj K, Pankaj Malhotra, Amit Singh, Cho-Jui Hsieh, Rohit Babbar

Abstract: Extreme Multi-label Classification (XMC) involves predicting a subset of relevant labels from an extremely large label space, given an input query and labels with textual features. Models developed for this problem have conventionally made use of dual encoder (DE) to embed the queries and label texts and one-vs-all (OvA) classifiers to rerank the shortlisted labels by the DE. While such methods ha… ▽ More Extreme Multi-label Classification (XMC) involves predicting a subset of relevant labels from an extremely large label space, given an input query and labels with textual features. Models developed for this problem have conventionally made use of dual encoder (DE) to embed the queries and label texts and one-vs-all (OvA) classifiers to rerank the shortlisted labels by the DE. While such methods have shown empirical success, a major drawback is their computational cost, often requiring upto 16 GPUs to train on the largest public dataset. Such a high cost is a consequence of calculating the loss over the entire label space. While shortlisting strategies have been proposed for classifiers, we aim to study such methods for the DE framework. In this work, we develop UniDEC, a loss-independent, end-to-end trainable framework which trains the DE and classifier together in a unified manner with a multi-class loss, while reducing the computational cost by 4-16x. This is done via the proposed pick-some-label (PSL) reduction, which aims to compute the loss on only a subset of positive and negative labels. These labels are carefully chosen in-batch so as to maximise their supervisory signals. Not only does the proposed framework achieve state-of-the-art results on datasets with labels in the order of millions, it is also computationally and resource efficient in achieving this performance on a single GPU. Code is made available at https://github.com/the-catalyst/UniDEC. △ Less

Submitted 3 March, 2025; v1 submitted 4 May, 2024; originally announced May 2024.

Journal ref: In Proceedings of the ACM Web Conference 2025 (WWW 2025)

CHC-COMP 2023: Competition Report

Authors: Emanuele De Angelis, Hari Govind V K

Abstract: CHC-COMP 2023 is the sixth edition of the Competition of Solvers for Constrained Horn Clauses. The competition was run in April 2023 and the results were presented at the 10th Workshop on Horn Clauses for Verification and Synthesis held in Paris, France, on April 23, 2023. This edition featured seven solvers (six competing and one hors concours) and six tracks, each of which dealing with a class o… ▽ More CHC-COMP 2023 is the sixth edition of the Competition of Solvers for Constrained Horn Clauses. The competition was run in April 2023 and the results were presented at the 10th Workshop on Horn Clauses for Verification and Synthesis held in Paris, France, on April 23, 2023. This edition featured seven solvers (six competing and one hors concours) and six tracks, each of which dealing with a class of clauses. This report describes the organization of CHC-COMP 2023 and presents its results. △ Less

Submitted 23 April, 2024; originally announced April 2024.

Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672

Journal ref: EPTCS 402, 2024, pp. 83-104

Speculative SAT Modulo SAT

Authors: Hari Govind V K, Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel

Abstract: State-of-the-art model-checking algorithms like IC3/PDR are based on uni-directional modular SAT solving for finding and/or blocking counterexamples. Modular SAT solvers divide a SAT-query into multiple sub-queries, each solved by a separate SAT solver (called a module), and propagate information (lemmas, proof obligations, blocked clauses, etc.) between modules. While modular solving is key to IC… ▽ More State-of-the-art model-checking algorithms like IC3/PDR are based on uni-directional modular SAT solving for finding and/or blocking counterexamples. Modular SAT solvers divide a SAT-query into multiple sub-queries, each solved by a separate SAT solver (called a module), and propagate information (lemmas, proof obligations, blocked clauses, etc.) between modules. While modular solving is key to IC3/PDR, it is obviously not as effective as monolithic solving, especially when individual sub-queries are harder to solve than the combined query. This is partially addressed in SAT modulo SAT (SMS) by propagating unit literals back and forth between the modules and using information from one module to simplify the sub-query in another module as soon as possible (i.e., before the satisfiability of any sub-query is established). However, bi-directionality of SMS is limited because of the strict order between decisions and propagation -- only one module is allowed to make decisions, until its sub-query is SAT. In this paper, we propose a generalization of SMS, called SPEC SMS, that speculates decisions between modules. This makes it bi-directional -- decisions are made in multiple modules, and learned clauses are exchanged in both directions. We further extend DRUP proofs and interpolation, these are useful in model checking, to SPEC SMS. We have implemented SPEC SMS in Z3 and show that it performs exponentially better on a series of benchmarks that are provably hard for SMS. △ Less

Submitted 30 June, 2023; originally announced June 2023.

Fast Approximations of Quantifier Elimination

Authors: Isabel Garcia-Contreras, Hari Govind V K, Sharon Shoham, Arie Gurfinkel

Abstract: Quantifier elimination (qelim) is used in many automated reasoning tasks including program synthesis, exist-forall solving, quantified SMT, Model Checking, and solving Constrained Horn Clauses (CHCs). Exact qelim is computationally expensive. Hence, it is often approximated. For example, Z3 uses "light" pre-processing to reduce the number of quantified variables. CHC-solver Spacer uses model-based… ▽ More Quantifier elimination (qelim) is used in many automated reasoning tasks including program synthesis, exist-forall solving, quantified SMT, Model Checking, and solving Constrained Horn Clauses (CHCs). Exact qelim is computationally expensive. Hence, it is often approximated. For example, Z3 uses "light" pre-processing to reduce the number of quantified variables. CHC-solver Spacer uses model-based projection (MBP) to under-approximate qelim relative to a given model, and over-approximations of qelim can be used as abstractions. In this paper, we present the QEL framework for fast approximations of qelim. QEL provides a uniform interface for both quantifier reduction and model-based projection. QEL builds on the egraph data structure -- the core of the EUF decision procedure in SMT -- by casting quantifier reduction as a problem of choosing ground (i.e., variable-free) representatives for equivalence classes. We have used QEL to implement MBP for the theories of Arrays and Algebraic Data Types (ADTs). We integrated QEL and our new MBP in Z3 and evaluated it within several tasks that rely on quantifier approximations, outperforming state-of-the-art. △ Less

Submitted 16 June, 2023; originally announced June 2023.

Comments: Published at CAV 2023

Localisation of Mammographic masses by Greedy Backtracking of Activations in the Stacked Auto-Encoders

Authors: Shamna Pootheri, Govindan V K

Abstract: Mammographic image analysis requires accurate localisation of salient mammographic masses. In mammographic computer-aided diagnosis, mass or Region of Interest (ROI) is often marked by physicians and features are extracted from the marked ROI. In this paper, we present a novel mammographic mass localisation framework, based on the maximal class activations of the stacked auto-encoders. We hypothes… ▽ More Mammographic image analysis requires accurate localisation of salient mammographic masses. In mammographic computer-aided diagnosis, mass or Region of Interest (ROI) is often marked by physicians and features are extracted from the marked ROI. In this paper, we present a novel mammographic mass localisation framework, based on the maximal class activations of the stacked auto-encoders. We hypothesize that the image regions activating abnormal classes in mammographic images will be the breast masses which causes the anomaly. The experiment is conducted using randomly selected 200 mammographic images (100 normal and 100 abnormal) from IRMA mammographic dataset. Abnormal mass regions marked by an expert radiologist are used as the ground truth. The proposed method outperforms existing Deep Convolutional Neural Network (DCNN) based techniques in terms of salient region detection accuracy. The proposed greedy backtracking method is more efficient and does not require a vast number of labelled training images as in DCNN based method. Such automatic localisation method will assist physicians to make accurate decisions on biopsy recommendations and treatment evaluations. △ Less

Submitted 8 May, 2023; originally announced May 2023.

CHC-COMP 2022: Competition Report

Authors: Emanuele De Angelis, Hari Govind V K

Abstract: CHC-COMP 2022 is the fifth edition of the competition of solvers for Constrained Horn Clauses. The competition was run in March 2022; the results were presented at the 9th Workshop on Horn Clauses for Verification and Synthesis held in Munich, Germany, on April 3, 2022. This edition featured six solvers, and eight tracks consisting of sets of linear and nonlinear clauses with constraints over line… ▽ More CHC-COMP 2022 is the fifth edition of the competition of solvers for Constrained Horn Clauses. The competition was run in March 2022; the results were presented at the 9th Workshop on Horn Clauses for Verification and Synthesis held in Munich, Germany, on April 3, 2022. This edition featured six solvers, and eight tracks consisting of sets of linear and nonlinear clauses with constraints over linear integer arithmetic, linear real arithmetic, arrays, and algebraic data types. This report provides an overview of the organization behind the competition runs: it includes the technical details of the competition setup as well as presenting the results of the 2022 edition. △ Less

Submitted 22 November, 2022; originally announced November 2022.

Comments: In Proceedings HCVS/VPT 2022, arXiv:2211.10675. arXiv admin note: text overlap with arXiv:2109.04635, arXiv:2008.02939 by other authors

ACM Class: F.3.1

Journal ref: EPTCS 373, 2022, pp. 44-62

Unified Generative & Dense Retrieval for Query Rewriting in Sponsored Search

Authors: Akash Kumar Mohankumar, Bhargav Dodla, Gururaj K, Amit Singh

Abstract: Sponsored search is a key revenue source for search engines, where advertisers bid on keywords to target users or search queries of interest. However, finding relevant keywords for a given query is challenging due to the large and dynamic keyword space, ambiguous user/advertiser intents, and diverse possible topics and languages. In this work, we present a comprehensive comparison between two para… ▽ More Sponsored search is a key revenue source for search engines, where advertisers bid on keywords to target users or search queries of interest. However, finding relevant keywords for a given query is challenging due to the large and dynamic keyword space, ambiguous user/advertiser intents, and diverse possible topics and languages. In this work, we present a comprehensive comparison between two paradigms for online query rewriting: Generative (NLG) and Dense Retrieval (DR) methods. We observe that both methods offer complementary benefits that are additive. As a result, we show that around 40% of the high-quality keywords retrieved by the two approaches are unique and not retrieved by the other. To leverage the strengths of both methods, we propose CLOVER-Unity, a novel approach that unifies generative and dense retrieval methods in one single model. Through offline experiments, we show that the NLG and DR components of CLOVER-Unity consistently outperform individually trained NLG and DR models on public and internal benchmarks. Furthermore, we show that CLOVER-Unity achieves 9.8% higher good keyword density than the ensemble of two separate DR and NLG models while reducing computational costs by almost half. We conduct extensive online A/B experiments on Microsoft Bing in 140+ countries and achieve improved user engagement, with an average increase in total clicks by 0.89% and increased revenue by 1.27%. We also share our practical lessons and optimization tricks for deploying such unified models in production. △ Less

Submitted 3 June, 2023; v1 submitted 13 September, 2022; originally announced September 2022.

Comments: 7 pages, 4 figures and 6 tables

NGAME: Negative Mining-aware Mini-batching for Extreme Classification

Authors: Kunal Dahiya, Nilesh Gupta, Deepak Saini, Akshay Soni, Yajun Wang, Kushal Dave, Jian Jiao, Gururaj K, Prasenjit Dey, Amit Singh, Deepesh Hada, Vidit Jain, Bhawna Paliwal, Anshul Mittal, Sonu Mehta, Ramachandran Ramjee, Sumeet Agarwal, Purushottam Kar, Manik Varma

Abstract: Extreme Classification (XC) seeks to tag data points with the most relevant subset of labels from an extremely large label set. Performing deep XC with dense, learnt representations for data points and labels has attracted much attention due to its superiority over earlier XC methods that used sparse, hand-crafted features. Negative mining techniques have emerged as a critical component of all dee… ▽ More Extreme Classification (XC) seeks to tag data points with the most relevant subset of labels from an extremely large label set. Performing deep XC with dense, learnt representations for data points and labels has attracted much attention due to its superiority over earlier XC methods that used sparse, hand-crafted features. Negative mining techniques have emerged as a critical component of all deep XC methods that allow them to scale to millions of labels. However, despite recent advances, training deep XC models with large encoder architectures such as transformers remains challenging. This paper identifies that memory overheads of popular negative mining techniques often force mini-batch sizes to remain small and slow training down. In response, this paper introduces NGAME, a light-weight mini-batch creation technique that offers provably accurate in-batch negative samples. This allows training with larger mini-batches offering significantly faster convergence and higher accuracies than existing negative sampling techniques. NGAME was found to be up to 16% more accurate than state-of-the-art methods on a wide array of benchmark datasets for extreme classification, as well as 3% more accurate at retrieving search engine queries in response to a user webpage visit to show personalized ads. In live A/B tests on a popular search engine, NGAME yielded up to 23% gains in click-through-rates. △ Less

Submitted 10 July, 2022; originally announced July 2022.

Bi-Sampling Approach to Classify Music Mood leveraging Raga-Rasa Association in Indian Classical Music

Authors: Mohan Rao B C, Vinayak Arkachaari, Harsha M N, Sushmitha M N, Gayathri Ramesh K K, Ullas M S, Pathi Mohan Rao, Sudha G, Narayana Darapaneni

Abstract: The impact of Music on the mood or emotion of the listener is a well-researched area in human psychology and behavioral science. In Indian classical music, ragas are the melodic structure that defines the various styles and forms of the music. Each raga has been found to evoke a specific emotion in the listener. With the advent of advanced capabilities of audio signal processing and the applicatio… ▽ More The impact of Music on the mood or emotion of the listener is a well-researched area in human psychology and behavioral science. In Indian classical music, ragas are the melodic structure that defines the various styles and forms of the music. Each raga has been found to evoke a specific emotion in the listener. With the advent of advanced capabilities of audio signal processing and the application of machine learning, the demand for intelligent music classifiers and recommenders has received increased attention, especially in the 'Music as a service' cloud applications. This paper explores a novel framework to leverage the raga-rasa association in Indian classical Music to build an intelligent classifier and its application in music recommendation system based on user's current mood and the mood they aspire to be in. △ Less

Submitted 13 March, 2022; originally announced March 2022.

Interference-Aware Accurate Signal Recovery in sub-1 GHz UHF Band Reuse-1 Cellular OFDMA Downlinks

Authors: Abhay Mohan M V, Giridhar K

Abstract: Reuse-1 systems operating in the sub-1 GHz UHF band are limited by substantial co-channel interference (CCI). In such orthogonal frequency division multiple access (OFDMA) cellular systems, the inter-sector or inter-tower interference (ITI) makes accurate signal recovery quite challenging as sub-1 GHz bands only support single-input single-output (SISO) links. Interference-aware receiver algorithm… ▽ More Reuse-1 systems operating in the sub-1 GHz UHF band are limited by substantial co-channel interference (CCI). In such orthogonal frequency division multiple access (OFDMA) cellular systems, the inter-sector or inter-tower interference (ITI) makes accurate signal recovery quite challenging as sub-1 GHz bands only support single-input single-output (SISO) links. Interference-aware receiver algorithms are essential to mitigate the ITI in such low-frequency bands. Such algorithms enable ubiquitous mobile broadband access over the entire homeland, say with >95% geographical coverage with quality of service guarantees. One element of the interference-aware signal recovery is the least-squares-based joint channel estimation scheme that uses non-orthogonal pilot subcarriers. This estimator is then compared with a variant that uses orthogonal pilot subcarriers to bring out the advantage of this joint estimator. It is shown that the proposed joint estimator requires fewer pilots to be well-determined when compared to its under-determined orthogonal counterpart. Moreover, it is easy to implement and does not require any knowledge of channel statistics. This work also derives a compensation factor needed for the interference-aware detector in the presence of inter-carrier interference (ICI) originating from multiple transmitters. Simulation results show that the proposed joint channel estimator outperforms traditional estimators at moderate to high frequency selectivity. The proposed compensation factor to the joint detector is found to be essential for recovering the transmitted signal in the absence of phase-tracking pilots. △ Less

Submitted 15 November, 2022; v1 submitted 1 August, 2021; originally announced August 2021.

Comments: in IEEE Open Journal of the Communications Society, 2022

Journal ref: IEEE Open Journal of the Communications Society, 2022

Logical Characterization of Coherent Uninterpreted Programs

Authors: Hari Govind V K, Sharon Shoham, Arie Gurfinkel

Abstract: An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compiler optimization, and program verification. While simple, the model is sufficiently powerful to encode counter automata, and, hence, undecidable. Recently, a class of UP programs, called coherent, has been proposed and sho… ▽ More An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compiler optimization, and program verification. While simple, the model is sufficiently powerful to encode counter automata, and, hence, undecidable. Recently, a class of UP programs, called coherent, has been proposed and shown to be decidable. We provide an alternative, logical characterization, of this result. Specifically, we show that every coherent program is bisimilar to a finite state system. Moreover, an inductive invariant of a coherent program is representable by a formula whose terms are of depth at most 1. We also show that the original proof, via automata, only applies to programs over unary uninterpreted functions. While this work is purely theoretical, it suggests a novel abstraction that is complete for coherent programs but can be soundly used on arbitrary uninterpreted (and partially interpreted) programs. △ Less

Submitted 25 July, 2021; originally announced July 2021.

Comments: Accepted at FMCAD 2021

A Review of Link Aggregation Control Protocol (LACP) as a Link Redundancy in SDN Based Network Using Ryu-Controller

Authors: Ali Ibnun Nurhadi, Guntur Petrus B. K., Muhammad Firdaus, Raditya Muhammad

Abstract: A reliable network is an absolute requirement for telecommunication networks at this time. This is in line with the growing number of users who need a reliable and uninterrupted connection to the server. Link Aggregation is one of the techniques that can be used to provide a reliable network. Link Aggregation System combines two or more links into one logical link, which is characterized by the us… ▽ More A reliable network is an absolute requirement for telecommunication networks at this time. This is in line with the growing number of users who need a reliable and uninterrupted connection to the server. Link Aggregation is one of the techniques that can be used to provide a reliable network. Link Aggregation System combines two or more links into one logical link, which is characterized by the use of a single IP address. During the communication between host and server, whenever the used link is broken or terminated the other active link can act as redundancy to resume that communication. This mechanism is called link redundancy. This mechanism will not run without the existence of another mechanism that monitors the condition of the links, which is either connected or disconnected. That mechanism is called link monitoring. Link monitoring used in this simulation is the Media Independent Interface (MII). In this simulation, we used Ryu-Controller and mininet Simulator to test the reliability of Link Aggregation-based SDN (Software Defined Network). During the simulation, we analyzed failover performance and how the Link Aggregation distributes the connection across the links for every which comes from a different source. From the simulations, we confirmed that link redundancy, the same data rate for every connection, to some degree, worked as intended. △ Less

Submitted 23 May, 2020; originally announced May 2020.

Global Guidance for Local Generalization in Model Checking

Authors: Hari Govind V K, YuTing Chen, Sharon Shoham, Arie Gurfinkel

Abstract: SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants via local reasoning about a single step of the transition relation of a system, while employing SMT-based procedures, such as interpolation, to mitigate the limitations of local reasoning and allow for better generalizat… ▽ More SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants via local reasoning about a single step of the transition relation of a system, while employing SMT-based procedures, such as interpolation, to mitigate the limitations of local reasoning and allow for better generalization. Unfortunately, these mitigations intertwine model checking with heuristics of the underlying SMT-solver, negatively affecting stability of model checking. In this paper, we propose to tackle the limitations of locality in a systematic manner. We introduce explicit global guidance into the local reasoning performed by IC3-style algorithms. To this end, we extend the SMT-IC3 paradigm with three novel rules, designed to mitigate fundamental sources of failure that stem from locality. We instantiate these rules for the theory of Linear Integer Arithmetic and implement them on top of SPACER solver in Z3. Our empirical results show that GSPACER, SPACER extended with global guidance, is significantly more effective than both SPACER and sole global reasoning, and, furthermore, is insensitive to interpolation. △ Less

Submitted 27 May, 2020; originally announced May 2020.

Comments: Published in CAV 2020

Computer Vision-based Accident Detection in Traffic Surveillance

Authors: Earnest Paul Ijjina, Dhananjai Chand, Savyasachi Gupta, Goutham K

Abstract: Computer vision-based accident detection through video surveillance has become a beneficial but daunting task. In this paper, a neoteric framework for detection of road accidents is proposed. The proposed framework capitalizes on Mask R-CNN for accurate object detection followed by an efficient centroid based object tracking algorithm for surveillance footage. The probability of an accident is det… ▽ More Computer vision-based accident detection through video surveillance has become a beneficial but daunting task. In this paper, a neoteric framework for detection of road accidents is proposed. The proposed framework capitalizes on Mask R-CNN for accurate object detection followed by an efficient centroid based object tracking algorithm for surveillance footage. The probability of an accident is determined based on speed and trajectory anomalies in a vehicle after an overlap with other vehicles. The proposed framework provides a robust method to achieve a high Detection Rate and a low False Alarm Rate on general road-traffic CCTV surveillance footage. This framework was evaluated on diverse conditions such as broad daylight, low visibility, rain, hail, and snow using the proposed dataset. This framework was found effective and paves the way to the development of general-purpose vehicular accident detection algorithms in real-time. △ Less

Submitted 22 November, 2019; originally announced November 2019.

Comments: Accepted in 10th ICCCNT 2019

Journal ref: 10th ICCCNT, 2019, pp. 1-6

Equipping SBMs with RBMs: An Explainable Approach for Analysis of Networks with Covariates

Authors: Shubham Gupta, Gururaj K., Ambedkar Dukkipati, Rui M. Castro

Abstract: Networks with node covariates offer two advantages to community detection methods, namely, (i) exploit covariates to improve the quality of communities, and more importantly, (ii) explain the discovered communities by identifying the relative importance of different covariates in them. Recent methods have almost exclusively focused on the first point above. However, the quantitative improvements o… ▽ More Networks with node covariates offer two advantages to community detection methods, namely, (i) exploit covariates to improve the quality of communities, and more importantly, (ii) explain the discovered communities by identifying the relative importance of different covariates in them. Recent methods have almost exclusively focused on the first point above. However, the quantitative improvements offered by them are often due to complex black-box models like deep neural networks at the expense of explainability. Approaches that focus on the second point are either domain-specific or have poor performance in practice. This paper proposes explainable, domain-independent statistical models for networks with node covariates that additionally offer good quantitative performance. Our models combine the strengths of Stochastic Block Models and Restricted Boltzmann Machines to provide interpretable insights about the communities. They support both pure and mixed community memberships. Besides providing explainability, our approach's main strength is that it does not explicitly assume a causal direction between community memberships and node covariates, making it applicable in diverse domains. We derive efficient inference procedures for our models, which can, in some cases, run in linear time in the number of nodes and edges. Experiments on several synthetic and real-world networks demonstrate that our models achieve close to state-of-the-art performance on community detection and link prediction tasks while also providing explanations for the discovered communities. △ Less

Submitted 5 April, 2021; v1 submitted 11 November, 2019; originally announced November 2019.

Interpolating Strong Induction

Authors: Hari Govind V K, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel

Abstract: The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened, there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based… ▽ More The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened, there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based on interpolation and property directed reachability (Pdr). In this paper, we present kAvy, an SMC algorithm that effectively uses k-induction to guide interpolation and Pdr-style inductive generalization. Unlike pure k-induction, kAvy uses Pdr-style generalization to compute and strengthen an inductive trace. Unlike pure Pdr, kAvy uses relative k-induction to construct an inductive invariant. The depth of induction is adjusted dynamically by minimizing a proof of unsatisfiability. We have implemented kAvy within the Avy Model Checker and evaluated it on HWMCC instances. Our results show that kAvy is more effective than both Avy and Pdr, and that using k-induction leads to faster running time and solving more instances. Further, on a class of benchmarks, called shift, kAvy is orders of magnitude faster than Avy, Pdr and k-induction. △ Less

Submitted 4 June, 2019; originally announced June 2019.

Comments: Accepted to CAV 19

Twin Sort Technique

Authors: Veeresh D, Thimmaraju S. N, Ravish G. K

Abstract: The objective behind the Twin Sort technique is to sort the list of unordered data elements efficiently and to allow efficient and simple arrangement of data elements within the data structure with optimization of comparisons and iterations in the sorting method. This sorting technique effectively terminates the iterations when there is no need of comparison if the elements are all sorted in betwe… ▽ More The objective behind the Twin Sort technique is to sort the list of unordered data elements efficiently and to allow efficient and simple arrangement of data elements within the data structure with optimization of comparisons and iterations in the sorting method. This sorting technique effectively terminates the iterations when there is no need of comparison if the elements are all sorted in between the iterations. Unlike Quick sort, Merge sorting technique, this new sorting technique is based on the iterative method of sorting elements within the data structure. So it will be advantageous for optimization of iterations when there is no need for sorting elements. Finally, the Twin Sort technique is more efficient and simple method of arranging elements within a data structure and it is easy to implement when comparing to the other sorting technique. By the introduction of optimization of comparison and iterations, it will never allow the arranging task on the ordered elements. △ Less

Submitted 22 October, 2017; originally announced October 2017.

Comments: core computer algorithm, 3 pages, conference

Journal ref: International Journal of Combined Research & Development October 2014

Modeling and Simulation of the Dynamics of the Quick Return Mechanism: A Bond Graph Approach

Authors: Anand Vaz, Thommen G K

Abstract: This paper applies the multibond graph approach for rigid multibody systems to model the dynamics of general spatial mechanisms. The commonly used quick return mechanism which comprises of revolute as well as prismatic joints has been chosen as a representative example to demonstrate the application of this technique and its resulting advantages. In this work, the links of the quick return mechani… ▽ More This paper applies the multibond graph approach for rigid multibody systems to model the dynamics of general spatial mechanisms. The commonly used quick return mechanism which comprises of revolute as well as prismatic joints has been chosen as a representative example to demonstrate the application of this technique and its resulting advantages. In this work, the links of the quick return mechanism are modeled as rigid bodies. The rigid links are then coupled at the joints based on the nature of constraint. This alternative method of formulation of system dynamics, using Bond Graphs, offers a rich set of features that include pictorial representation of the dynamics of translation and rotation for each link of the mechanism in the inertial frame, representation and handling of constraints at the joints, depiction of causality, obtaining dynamic reaction forces and moments at various locations in the mechanism and so on. Yet another advantage of this approach is that the coding for simulation can be carried out directly from the Bond Graph in an algorithmic manner, without deriving system equations. In this work, the program code for simulation is written in MATLAB. The vector and tensor operations are conveniently represented in MATLAB, resulting in a compact and optimized code. The simulation results are plotted and discussed in detail. △ Less

Submitted 22 May, 2017; originally announced May 2017.

Comments: Document prepared for National Conference on Industrial Problems on Machines and Mechanisms (2010), 8 pages, 19 Figures

Journal ref: Proceedings of 10th National Conference on Industrial Problems on Machines and Mechanisms (IPRoMM 2010), MNIT, Jaipur, Rajasthan, December 17-18,2010, paper No. IPRoMM 2010-34, p. 23-30

HellRank: A Hellinger-based Centrality Measure for Bipartite Social Networks

Authors: Seyed Mohammad Taheri, Hamidreza Mahyar, Mohammad Firouzi, Elahe Ghalebi K., Radu Grosu, Ali Movaghar

Abstract: Measuring centrality in a social network, especially in bipartite mode, poses several challenges such as requirement of full knowledge of the network topology and lack of properly detection of top-k behavioral representative users. In this paper, to overcome the aforementioned challenging issues, we propose an accurate centrality measure, called HellRank, to identify central nodes in bipartite soc… ▽ More Measuring centrality in a social network, especially in bipartite mode, poses several challenges such as requirement of full knowledge of the network topology and lack of properly detection of top-k behavioral representative users. In this paper, to overcome the aforementioned challenging issues, we propose an accurate centrality measure, called HellRank, to identify central nodes in bipartite social networks. HellRank is based on the Hellinger distance between two nodes on the same side of a bipartite network. We theoretically analyze the impact of the Hellinger distance on a bipartite network and find an upper and lower bounds for this distance. The computation of HellRank centrality measure can be distributed by letting each node uses only local information on its immediate neighbors and therefore do not need a central entity to have full knowledge of the network topological structure. We experimentally evaluate performance of the HellRank measure in correlation with other centrality measures on real-world networks. The results show partial ranking similarity between the HellRank and the other conventional metrics according to the Kendall and Spearman rank correlation coefficient. △ Less

Submitted 17 March, 2017; v1 submitted 5 December, 2016; originally announced December 2016.

Journal ref: Soc. Netw. Anal. Min. (2017) 7: 22

Extracting Implicit Social Relation for Social Recommendation Techniques in User Rating Prediction

Authors: Seyed Mohammad Taheri, Hamidreza Mahyar, Mohammad Firouzi, Elahe Ghalebi K., Radu Grosu, Ali Movaghar

Abstract: Recommendation plays an increasingly important role in our daily lives. Recommender systems automatically suggest items to users that might be interesting for them. Recent studies illustrate that incorporating social trust in Matrix Factorization methods demonstrably improves accuracy of rating prediction. Such approaches mainly use the trust scores explicitly expressed by users. However, it is of… ▽ More Recommendation plays an increasingly important role in our daily lives. Recommender systems automatically suggest items to users that might be interesting for them. Recent studies illustrate that incorporating social trust in Matrix Factorization methods demonstrably improves accuracy of rating prediction. Such approaches mainly use the trust scores explicitly expressed by users. However, it is often challenging to have users provide explicit trust scores of each other. There exist quite a few works, which propose Trust Metrics to compute and predict trust scores between users based on their interactions. In this paper, first we present how social relation can be extracted from users' ratings to items by describing Hellinger distance between users in recommender systems. Then, we propose to incorporate the predicted trust scores into social matrix factorization models. By analyzing social relation extraction from three well-known real-world datasets, which both: trust and recommendation data available, we conclude that using the implicit social relation in social recommendation techniques has almost the same performance compared to the actual trust scores explicitly expressed by users. Hence, we build our method, called Hell-TrustSVD, on top of the state-of-the-art social recommendation technique to incorporate both the extracted implicit social relations and ratings given by users on the prediction of items for an active user. To the best of our knowledge, this is the first work to extend TrustSVD with extracted social trust information. The experimental results support the idea of employing implicit trust into matrix factorization whenever explicit trust is not available, can perform much better than the state-of-the-art approaches in user rating prediction. △ Less

Submitted 17 March, 2017; v1 submitted 5 December, 2016; originally announced December 2016.

Implementation of linear detection techniques to overcome channel effects in MIMO

Authors: Gopika K, M Mathurakani

Abstract: Spatial diversity technique enables improvement in quality and reliability of wireless link. Antenna diversity along with understanding effects of channel on transmitted signal and methods to overcome the channel impairment plays an important role in wireless communication where sharing of channel occurs between users. In this paper single input single output system (SISO) is compared with multipl… ▽ More Spatial diversity technique enables improvement in quality and reliability of wireless link. Antenna diversity along with understanding effects of channel on transmitted signal and methods to overcome the channel impairment plays an important role in wireless communication where sharing of channel occurs between users. In this paper single input single output system (SISO) is compared with multiple input multiple output system (MIMO) in terms of bit error rate performance. Bit error rate performance is also evaluated for MIMO with least squares (LS) and Minimum mean square error (MMSE) linear detection. Further analysis and simulation is done to understand the effect of channel imperfections on BER. △ Less

Submitted 10 May, 2016; originally announced May 2016.

Comments: 10 pages,7 figures, explanation for all figures given