VLDB 2026 Research / reviewers in the wild / expert
Chirag Agarwal
dblp:173/8821
· DBLP profile ↗
28ranked-venue papers
9as first author
22since 2021 · last 2026
0000-0002-6354-7260ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Artificial intelligence and machine learning · 22 · 6 first-author · 20 since 2021Graphics, computer vision, multimedia, augmented reality and games · 9 · 5 first-author · 4 since 2021Human-computer interaction and ubiquitous computing · 2 · 2 since 2021Software engineering, systems software and programming languages · 1 · 1 first-authorDatabases, data management, data science and information retrieval · 1 · 1 since 2021Theory of computation · 1 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Towards Trustworthy Multimodal AI SystemsabstractMachine learning models have become ubiquitous in the last decade, and with their increasing use in critical applications (e.g., healthcare, financial systems, and crime forecasting), it is vital to ensure that ML developers and practitioners understand and trust their decisions. This problem has become paramount in the era of frontier models, which are developed by training billion-parameter models on broad, uncurated datasets and extensive computing. In this talk, we will first explore the (un)reliability of existing multimodal explainability techniques in large language and multimodal models and understand the robustness and safety implications of Mechanistic Interpretability tools. Next, we will delve into two complementary threads: i) domain-specific safety and related trustworthy evaluation that surfaces risks missed by generic red-teaming, focusing on multilingual and distribution-shifted settings; and ii) methods that explicitly train and assess reasoning in medical LLMs. Chirag Agarwal |
AAAI | 1 |
| 2026 | Polarity-Aware Probing for Quantifying Latent Alignment in Language ModelsabstractAdvances in unsupervised probes like Contrast‑Consistent Search (CCS), which reveal latent beliefs without token outputs, raise the question of whether they can reliably assess model alignment. We investigate this by examining CCS's sensitivity to harmful vs. safe statements and introducing Polarity‑Aware CCS (PA‑CCS), which evaluates whether a model's internal representations remain consistent under polarity inversion. We propose two alignment-oriented metrics -- Polar‑Consistency and Contradiction Index -- to quantify the semantic robustness of a model's latent knowledge. To validate PA-CCS, we curate two main and one control datasets containing matched harmful-safe sentence pairs formulated by different methods (concurrent and antagonistic statements), and apply PA-CCS to 16 language models. Our results demonstrate that PA‑CCS reveals both architectural and layer-specific differences in the encoding of latent harmful knowledge. Interestingly, replacing the negation token with a meaningless marker degrades the PA‑CCS scores of models with aligned representations. In contrast, models lacking robust internal calibration do not show this degradation. Sabrina Sadiekh, Elena Ericheva, Chirag Agarwal |
AAAI | 3 |
| 2026 | CURE-Med: Curriculum-Informed Reinforcement Learning for Multilingual Medical ReasoningabstractEric Onyame, Akash Ghosh, Subhadip Baidya, Sriparna Saha, Xiuying Chen, Chirag Agarwal. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2026. Eric Onyame, Akash Ghosh, Subhadip Baidya, Sriparna Saha 0001, Xiuying Chen, Chirag Agarwal |
ACL (1) | 6 |
| 2026 | Improving Human Verification of LLM Reasoning through Interactive Explanation InterfacesabstractThe reasoning capabilities of Large Language Models (LLMs) have led to their increasing employment in several critical applications, particularly education, where they support problem-solving, tutoring, and personalized study. While there are a plethora of works showing the effectiveness of LLMs in generating step-by-step solutions through chain-of-thought (CoT) reasoning on reasoning benchmarks, little is understood about whether the generated CoT is helpful for end-users in improving their ability to comprehend mathematical reasoning problems and detect errors/hallucinations in LLM-generated solutions. To address this gap and contribute to understanding how reasoning can improve human-AI interaction, we present three new interactive reasoning interfaces: interactive CoT (iCoT), interactive Program-of-Thought (iPoT), and interactive Graph (iGraph), and a novel framework that generates the LLM’s reasoning from traditional CoT to alternative, interactive formats. Across 125 participants, we found that interactive interfaces significantly improved performance. Specifically, the iGraph interface yielded the highest clarity and error detection rate (\(85.6\%\)), followed by iPoT (\(82.5\%\)), iCoT (\(80.6\%\)), all outperforming standard CoT (\(73.5\%\)). Interactive interfaces also led to faster response times, where participants using iGraph were fastest (57.9 secs), compared to iCoT and iPoT (60 secs), and the standard CoT baseline (64.7 secs). Furthermore, participants preferred the iGraph reasoning interface, citing its superior ability to enable users to follow the LLM’s reasoning process. We discuss the implications of these results and provide recommendations for the future design of reasoning models. The code and interfaces for this project can be found here: https://github.com/Runtaozhou/Interactive-CoT Runtao Zhou, Giang Nguyen 0004, Nikita Kharya, Anh Totti Nguyen, Chirag Agarwal |
IUI | 5 |
| 2025 | EGOILLUSION: Benchmarking Hallucinations in Egocentric Video UnderstandingabstractAshish Seth, Utkarsh Tyagi, Ramaneswaran Selvakumar, Nishit Anand, Sonal Kumar, Sreyan Ghosh, Ramani Duraiswami, Chirag Agarwal, Dinesh Manocha. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing. 2025. Ashish Seth, Utkarsh Tyagi, Ramaneswaran S., Nishit Anand, Sonal Kumar, Sreyan Ghosh, Ramani Duraiswami, Chirag Agarwal, Dinesh Manocha |
EMNLP | 8 |
| 2025 | Towards Operationalizing Right to Data ProtectionabstractAbhinav Java, Simra Shahid, Chirag Agarwal. Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers). 2025. Abhinav Java, Simra Shahid, Chirag Agarwal |
NAACL (Long Papers) | 3 |
| 2025 | On the Impact of Fine-Tuning on Chain-of-Thought ReasoningabstractElita Lobo, Chirag Agarwal, Himabindu Lakkaraju. Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers). 2025. Elita A. Lobo, Chirag Agarwal, Himabindu Lakkaraju |
NAACL (Long Papers) | 2 |
| 2025 | Analyzing Memorization in Large Language Models through the Lens of Model AttributionabstractTarun Ram Menta, Susmit Agrawal, Chirag Agarwal. Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers). 2025. Tarun Ram Menta, Susmit Agrawal, Chirag Agarwal |
NAACL (Long Papers) | 3 |
| 2024 | On the Trade-offs between Adversarial Robustness and Actionable ExplanationsabstractAs machine learning models are increasingly being employed in various high-stakes settings, it becomes important to ensure that predictions of these models are not only adversarially robust, but also readily explainable to relevant stakeholders. However, it is unclear if these two notions can be simultaneously achieved or if there exist trade-offs between them. In this work, we make one of the first attempts at studying the impact of adversarially robust models on actionable explanations which provide end users with a means for recourse. We theoretically and empirically analyze the cost (ease of implementation) and validity (probability of obtaining a positive model prediction) of recourses output by state-of-the-art algorithms when the underlying models are adversarially robust vs. non-robust. More specifically, we derive theoretical bounds on the differences between the cost and the validity of the recourses generated by state-of-the-art algorithms for adversarially robust vs. non-robust linear and non-linear models. Our empirical results with multiple real-world datasets validate our theoretical results and show the impact of varying degrees of model robustness on the cost and validity of the resulting recourses. Our analyses demonstrate that adversarially robust models significantly increase the cost and reduce the validity of the resulting recourses, thus shedding light on the inherent trade-offs between adversarial robustness and actionable explanations. Satyapriya Krishna, Chirag Agarwal, Himabindu Lakkaraju |
AIES (1) | 2 |
| 2024 | Quantifying Uncertainty in Natural Language Explanations of Large Language ModelsabstractLarge Language Models (LLMs) are increasingly used as powerful tools for several high-stakes natural language processing (NLP) applications. Recent prompting works claim to elicit intermediate reasoning steps and key tokens that serve as proxy explanations for LLM predictions. However, there is no certainty whether these explanations are reliable and reflect the LLM’s behavior. In this work, we make one of the first attempts at quantifying the uncertainty in explanations of LLMs. To this end, we propose two novel metrics — Verbalized Uncertainty and Probing Uncertainty — to quantify the uncertainty of generated explanations. While verbalized uncertainty involves prompting the LLM to express its confidence in its explanations, probing uncertainty leverages sample and model perturbations as a means to quantify the uncertainty. Our empirical analysis of benchmark datasets reveals that verbalized uncertainty is not a reliable estimate of explanation confidence. Further, we show that the probing uncertainty estimates are correlated with the faithfulness of an explanation, with lower uncertainty corresponding to explanations with higher faithfulness. Our study provides insights into the challenges and opportunities of quantifying uncertainty in LLM explanations, contributing to the broader discussion of the trustworthiness of foundation models. Sree Harsha Tanneru, Chirag Agarwal, Himabindu Lakkaraju |
AISTATS | 2 |
| 2024 | Understanding the Effects of Iterative Prompting on TruthfulnessabstractThe development of Large Language Models (LLMs) has notably transformed numerous sectors, offering impressive text generation capabilities. Yet, the reliability and truthfulness of these models remain pressing concerns. To this end, we investigate iterative prompting, a strategy hypothesized to refine LLM responses, assessing its impact on LLM truthfulness, an area which has not been thoroughly explored. Our extensive experiments explore the intricacies of iterative prompting variants, examining their influence on the accuracy and calibration of model responses. Our findings reveal that naive prompting methods significantly undermine truthfulness, leading to exacerbated calibration errors. In response to these challenges, we introduce several prompting variants designed to address the identified issues. These variants demonstrate marked improvements over existing baselines, signaling a promising direction for future research. Our work provides a nuanced understanding of iterative prompting and introduces novel approaches to enhance the truthfulness of LLMs, thereby contributing to the development of more accurate and trustworthy AI systems Satyapriya Krishna, Chirag Agarwal, Himabindu Lakkaraju |
ICML | 2 |
| 2024 | MedSafetyBench: Evaluating and Improving the Medical Safety of Large Language ModelsabstractAs large language models (LLMs) develop increasingly sophisticated capabilities and find applications in medical settings, it becomes important to assess their medical safety due to their far-reaching implications for personal and public health, patient safety, and human rights. However, there is little to no understanding of the notion of medical safety in the context of LLMs, let alone how to evaluate and improve it. To address this gap, we first define the notion of medical safety in LLMs based on the Principles of Medical Ethics set forth by the American Medical Association. We then leverage this understanding to introduce MedSafetyBench, the first benchmark dataset designed to measure the medical safety of LLMs. We demonstrate the utility of MedSafetyBench by using it to evaluate and improve the medical safety of LLMs. Our results show that publicly-available medical LLMs do not meet standards of medical safety and that fine-tuning them using MedSafetyBench improves their medical safety while preserving their medical performance. By introducing this new benchmark dataset, our work enables a systematic study of the state of medical safety in LLMs and motivates future work in this area, paving the way to mitigate the safety risks of LLMs in medicine. The benchmark dataset and code are available at https://github.com/AI4LIFE-GROUP/med-safety-bench. Tessa Han, Aounon Kumar, Chirag Agarwal, Himabindu Lakkaraju |
NeurIPS | 3 |
| 2023 | DeAR: Debiasing Vision-Language Models with Additive ResidualsabstractLarge pre-trained vision-language models (VLMs) reduce the time for developing predictive models for various vision-grounded language downstream tasks by providing rich, adaptable image and text representations. However, these models suffer from societal biases owing to the skewed distribution of various identity groups in the training data. These biases manifest as the skewed similarity between the representations for specific text concepts and images of people of different identity groups and, therefore, limit the usefulness of such models in real-world high-stakes applications. In this work, we present Dear(Debiasing with Additive Residuals), a novel debiasing method that learns additive residual image representations to offset the original representations, ensuring fair output representations. In doing so, it reduces the ability of the representations to distinguish between the different identity groups. Further, we observe that the current fairness tests are performed on limited face image datasets that fail to indicate why a specific text concept should/should not apply to them. To bridge this gap and better evaluate Dear,we introduce the Protected Attribute Tag Association (pata)dataset - a new context-based bias benchmarking dataset for evaluating the fairness of large pre-trained VLMs. Additionally, Pataprovides visual context for a diverse human population in different scenarios with both positive and negative connotations. Experimental results for fairness and zero-shot performance preservation using multiple datasets demonstrate the efficacy of our framework. The dataset is released here. Ashish Seth, Mayur Hemani, Chirag Agarwal |
CVPR | 3 |
| 2023 | GNNDelete: A General Strategy for Unlearning in Graph Neural Networks
Jiali Cheng, George Dasoulas, Chirag Agarwal, Marinka Zitnik |
ICLR | 4 |
| 2023 | Explaining RL Decisions with Trajectories
Shripad V. Deshmukh, Arpan Dasgupta, Balaji Krishnamurthy, Chirag Agarwal, Georgios Theocharous, Jayakumar Subramanian |
ICLR | 5 |
| 2023 | Explain Like I am BM25: Interpreting a Dense Model's Ranked-List with a Sparse ApproximationabstractNeural retrieval models (NRMs) have been shown to outperform their statistical counterparts owing to their ability to capture semantic meaning via dense document representations. These models, however, suffer from poor interpretability as they do not rely on explicit term matching. As a form of local per-query explanations, we introduce the notion of equivalent queries that are generated by maximizing the similarity between the NRM's results and the result set of a sparse retrieval system with the equivalent query. We then compare this approach with existing methods such as RM3-based query expansion and contrast differences in retrieval effectiveness and in the terms generated by each approach. Michael Llordes, Debasis Ganguly, Sumit Bhatia, Chirag Agarwal |
SIGIR | 4 |
| 2022 | Probing GNN Explainers: A Rigorous Theoretical and Empirical Analysis of GNN Explanation MethodsabstractAs Graph Neural Networks (GNNs) are increasingly being employed in critical real-world applications, several methods have been proposed in recent literature to explain the predictions of these models. However, there has been little to no work on systematically analyzing the reliability of these methods. Here, we introduce the first-ever theoretical analysis of the reliability of state-of-the-art GNN explanation methods. More specifically, we theoretically analyze the behavior of various state-of-the-art GNN explanation methods with respect to several desirable properties (e.g., faithfulness, stability, and fairness preservation) and establish upper bounds on the violation of these properties. We also empirically validate our theoretical results using extensive experimentation with nine real-world graph datasets. Our empirical results further shed light on several interesting insights about the behavior of state-of-the-art GNN explanation methods. Chirag Agarwal, Marinka Zitnik, Himabindu Lakkaraju |
AISTATS | 1 |
| 2022 | Exploring Counterfactual Explanations Through the Lens of Adversarial Examples: A Theoretical and Empirical AnalysisabstractAs machine learning (ML) models becomemore widely deployed in high-stakes applications, counterfactual explanations have emerged as key tools for providing actionable model explanations in practice. Despite the growing popularity of counterfactual explanations, the theoretical understanding of these explanations is still lacking behind. In this work, we systematically analyze counterfactual explanations through the lens of adversarial examples. We do so by formalizing the similarities between popular counterfactual explanation and adversarial example generation methods identifying conditions when they are equivalent. We then derive upper bounds between the solutions output by counterfactual explanation and adversarial example generation methods, which we validate on several real world data sets. By establishing these theoretical and empirical similarities between counterfactual explanations and adversarial examples, our work raises fundamental questions about the design and development of existing counterfactual explanation algorithms. Martin Pawelczyk, Chirag Agarwal, Shalmali Joshi, Sohini Upadhyay, Himabindu Lakkaraju |
AISTATS | 2 |
| 2022 | Estimating Example Difficulty using Variance of GradientsabstractIn machine learning, a question of great interest is understanding what examples are challenging for a model to classify. Identifying atypical examples ensures the safe de-ployment of models, isolates samples that require further human inspection and provides interpretability into model behavior. In this work, we propose Variance of Gradients (VoG) as a valuable and efficient metric to rank data by difficulty and to surface a tractable subset of the most chal-lenging examples for human-in-the-loop auditing. We show that data points with high VoG scores are far more difficult for the model to learn and over-index on corrupted or mem-orized examples. Further, restricting the evaluation to the test set instances with the lowest VoG improves the model's generalization performance. Finally, we show that VoG is a valuable and efficient ranking for out-of-distribution detection. Chirag Agarwal, Daniel D'souza, Sara Hooker |
CVPR | 1 |
| 2022 | OpenXAI: Towards a Transparent Evaluation of Model ExplanationsabstractWhile several types of post hoc explanation methods have been proposed in recent literature, there is very little work on systematically benchmarking these methods. Here, we introduce OpenXAI, a comprehensive and extensible open-source framework for evaluating and benchmarking post hoc explanation methods. OpenXAI comprises of the following key components: (i) a flexible synthetic data generator and a collection of diverse real-world datasets, pre-trained models, and state-of-the-art feature attribution methods, (ii) open-source implementations of twenty-two quantitative metrics for evaluating faithfulness, stability (robustness), and fairness of explanation methods, and (iii) the first ever public XAI leaderboards to readily compare several explanation methods across a wide variety of metrics, models, and datasets. OpenXAI is easily extensible, as users can readily evaluate custom explanation methods and incorporate them into our leaderboards. Overall, OpenXAI provides an automated end-to-end pipeline that not only simplifies and standardizes the evaluation of post hoc explanation methods, but also promotes transparency and reproducibility in benchmarking these methods. While the first release of OpenXAI supports only tabular datasets, the explanation methods and metrics that we consider are general enough to be applicable to other data modalities. OpenXAI datasets and data loaders, implementations of state-of-the-art explanation methods and evaluation metrics, as well as leaderboards are publicly available at https://open-xai.github.io/. OpenXAI will be regularly updated to incorporate text and image datasets, other new metrics and explanation methods, and welcomes inputs from the community. Chirag Agarwal, Satyapriya Krishna, Eshika Saxena, Martin Pawelczyk, Nari Johnson, Isha Puri, Marinka Zitnik, Himabindu Lakkaraju |
NeurIPS | 1 |
| 2021 | Towards the Unification and Robustness of Perturbation and Gradient Based ExplanationsabstractAs machine learning black boxes are increasingly being deployed in critical domains such as healthcare and criminal justice, there has been a growing emphasis on developing techniques for explaining these black boxes in a post hoc manner. In this work, we analyze two popular post hoc interpretation techniques: SmoothGrad which is a gradient based method, and a variant of LIME which is a perturbation based method. More specifically, we derive explicit closed form expressions for the explanations output by these two methods and show that they both converge to the same explanation in expectation, i.e., when the number of perturbed samples used by these methods is large. We then leverage this connection to establish other desirable properties, such as robustness, for these techniques. We also derive finite sample complexity bounds for the number of perturbations required for these methods to converge to their expected explanation. Finally, we empirically validate our theory using extensive experimentation on both synthetic and real-world datasets. Sushant Agarwal, Shahin Jabbari, Chirag Agarwal, Sohini Upadhyay, Steven Z. Wu, Himabindu Lakkaraju |
ICML | 3 |
| 2021 | Towards a unified framework for fair and stable graph representation learningabstractAs the representations output by Graph Neural Networks (GNNs) are increasingly employed in real-world applications, it becomes important to ensure that these representations are fair and stable. In this work, we establish a key connection between counterfactual fairness and stability and leverage it to propose a novel framework, NIFTY (uNIfying Fairness and stabiliTY), which can be used with any GNN to learn fair and stable representations. We introduce a novel objective function that simultaneously accounts for fairness and stability and develop a layer-wise weight normalization using the Lipschitz constant to enhance neural message passing in GNNs. In doing so, we enforce fairness and stability both in the objective function as well as in the GNN architecture. Further, we show theoretically that our layer-wise weight normalization promotes counterfactual fairness and stability in the resulting representations. We introduce three new graph datasets comprising of high-stakes decisions in criminal justice and financial lending domains. Extensive experimentation with the above datasets demonstrates the efficacy of our framework. Chirag Agarwal, Himabindu Lakkaraju, Marinka Zitnik |
UAI | 1 |
| 2020 | Explaining Image Classifiers by Removing Input Features Using Generative Models
Chirag Agarwal, Anh Totti Nguyen |
ACCV (6) | 1 |
| 2020 | SAM: The Sensitivity of Attribution Methods to HyperparametersabstractAttribution methods can provide powerful insights into the reasons for a classifier's decision. We argue that a key desideratum of an explanation is its robustness to input hyperparameter changes that are often randomly set or empirically tuned. High sensitivity to arbitrary hyperparameter choices does not only impede reproducibility but also questions the correctness of an explanation and impairs the trust by end-users. In this paper, we provide a thorough empirical study on the sensitivity of existing attribution methods. We found an alarming trend that many methods are highly sensitive to changes in their common hyperparameters e.g. even changing a random seed can yield a different explanation! In contrast, explanations generated for robust classifiers that are trained to be invariant to pixel-wise perturbations are surprisingly more robust. Interestingly, such sensitivity is not reflected in the average explanation correctness scores over the entire dataset as commonly reported in the literature. Naman Bansal, Chirag Agarwal, Anh Totti Nguyen |
CVPR | 2 |
| 2020 | DEEP-URL: A Model-Aware Approach to Blind Deconvolution Based on Deep Unfolded Richardson-Lucy NetworkabstractThe lack of interpretability in current deep learning models causes serious concerns as they are extensively used for various life-critical applications. Hence, it is of paramount importance to develop interpretable deep learning models. In this paper, we consider the problem of blind deconvolution and propose a novel model-aware deep architecture that allows for the recovery of both the blur kernel and the sharp image from the blurred image. In particular, we propose the Deep Unfolded Richardson-Lucy (Deep-URL) framework - an interpretable deep-learning architecture that can be seen as an amalgamation of classical estimation technique and deep neural network, and consequently leads to improved performance. Our numerical investigations demonstrate significant improvement compared to state-of-the-art algorithms. Chirag Agarwal, Shahin Khobahi, Arindam Bose, Mojtaba Soltanalian, Dan Schonfeld |
ICIP | 1 |
| 2019 | Improving Robustness to Adversarial Examples by Encouraging Discriminative FeaturesabstractDeep neural networks (DNNs) have achieved state-of-the-art results in various pattern recognition tasks. However, they perform poorly on out-of-distribution adversarial examples i.e. inputs that are specifically crafted by an adversary to cause DNNs to misbehave, questioning the security and reliability of applications. In this paper, we hypothesize inter-class and intra-class feature variances to be one of the reasons behind the existence of adversarial examples. Additionally, learning low intra-class and high inter-class feature variance help classifiers learn decision boundaries that are more compact and leave less inter-class low-probability "pockets" in the feature space, i.e. less room for adversarial perturbations. We achieve this by imposing a center loss [1] in addition to the regular softmax cross-entropy loss while training a DNN classifier. Intuitively, the center loss encourages DNNs to simultaneously learn a center for the deep features of each class, and minimize the distances between the intra-class deep features and their corresponding class centers. Our results on state-of-the-art architectures tested on MNIST, CIFAR-10, and CIFAR-100 datasets confirm our hypothesis and highlight the importance of discriminative features in the existence of adversarial examples. Chirag Agarwal, Anh Totti Nguyen, Dan Schonfeld |
ICIP | 1 |
| 2017 | Convolutional neural network steganalysis's application to steganographyabstractThis paper presents a novel approach to increase the performance bounds of image steganography under the criteria of minimizing distortion. The proposed approach utilizes a steganalysis convolutional neural network (CNN) framework to understand an image's model and embed in less detectable regions to preserve the model. In other word, the trained steganalysis CNN is used to calculate derivatives of the statistical model of an image with respect to embedding changes. The experimental results show that the proposed algorithm outperforms previous state-of-the-art methods in a wide range of low relative payloads when compared with HUGO, S-UNIWARD, and HILL by the state-of-the-art steganalysis. Mehdi Sharifzadeh, Chirag Agarwal, Mohammed Aloraini, Dan Schonfeld |
VCIP | 2 |
| 2015 | Compositional Reasoning Gotchas in PracticeabstractModel checking has become a formal sign-off requirement in the verification plans of many hardware designs. For design sizes encountered in practice, compositional assume-guarantee reasoning is often necessary to achieve satisfactory results. However, many pitfalls exist that can create unsound or unexpected results for users of commercial model checking tools. Users need to watch out for circularity in properties, for dead-ends getting trimmed by tools, as well as understand the differences in proof composition for liveness and safety properties. We present many real design examples to illustrate these points, as well as describe our experiences with compositional reasoning in practice. Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson, Vigyan Singhal |
FMCAD | 1 |