Aarti Gupta - RankMe

193 papers A* 36A 32B 31C 6Misc 10Journal 40Unranked 34

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms. CoRR Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora
2026	J	`jnl`	Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification. CoRR Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin
2026	J	`jnl`	SecIC3: Customizing IC3 for Hardware Security Verification. CoRR Qinhan Tan, Akash Gaonkar, Yu-Wei Fan, Aarti Gupta, Sharad Malik
2025	Misc	`conf`	A Layered Formal Methods Approach to Answering Queue-related Queries. NSDI Divya Raghunathan, Maria Apostolaki, Aarti Gupta
2025	J	`jnl`	FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols. CoRR Yu-An Shih, Annie Lin, Aarti Gupta, Sharad Malik
2025	J	`jnl`	Hierarchical Formal Verification of Hardware. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Huaixi Lu, Yue Xing, Aarti Gupta, Sharad Malik
2024	J	`jnl`	Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. ACM Trans. Design Autom. Electr. Syst. Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Gus Henry Smith, Thierry Tambe, Akash Gaonkar, Vishal Canumalla, Andrew Cheung, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik
2024	A	`conf`	Automatic Generation of Cycle-Accurate Timing Models from RTL for Hardware Accelerators. ICCAD Yu Zeng, Aarti Gupta, Sharad Malik
2024	Misc	`conf`	Buffy: A Formal Language-Based Framework for Network Performance Analysis. HotNets Amir Seyhani, Junyi Zhao, Aarti Gupta, David Walker, Mina Tahmasbi Arashloo
2024	B	`conf`	Exact Scheduling to Minimize Off-Chip Data Movement for Deep Learning Accelerators. ASPDAC Yi Li, Aarti Gupta, Sharad Malik
2024	J	`jnl`	Kirigami, the Verifiable Art of Network Cutting. IEEE/ACM Trans. Netw. Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker
2024	J	`jnl`	Super-resolution on network telemetry time series. CoRR Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki
2024	A*	`conf`	Zoom2Net: Constrained Network Telemetry Imputation. SIGCOMM Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki
2023	—	`conf`	CaT: A Solver-Aided Compiler for Packet-Processing Pipelines. ASPLOS (3) Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta
2023	J	`jnl`	Combined Scheduling, Memory Allocation and Tensor Replacement for Minimizing Off-Chip Data Accesses of DNN Accelerators. CoRR Yi Li, Aarti Gupta, Sharad Malik
2023	A*	`conf`	INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms. DAC Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik
2023	J	`jnl`	Modular Control Plane Verification via Temporal Invariants. Proc. ACM Program. Lang. Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker
2023	J	`jnl`	Psym: Efficient Symbolic Exploration of Distributed Systems. Proc. ACM Program. Lang. Lauren Pick, Ankush Desai, Aarti Gupta
2023	J	`jnl`	SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications. ACM Trans. Design Autom. Electr. Syst. Huaixi Lu, Yue Xing, Aarti Gupta, Sharad Malik
2023	J	`jnl`	Synthesizing MILP Constraints for Efficient and Robust Optimization. Proc. ACM Program. Lang. Jingbo Wang, Aarti Gupta, Chao Wang
2023	Misc	`conf`	Towards Integrating Formal Methods into ML-Based Systems for Networking. HotNets Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki
2022	B	`conf`	ACORN: Network Control Plane Abstraction using Route Nondeterminism. FMCAD Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker
2022	J	`jnl`	ACORN: Network Control Plane Abstraction using Route Nondeterminism. CoRR Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker
2022	A	`conf`	Automatic Generation of Architecture-Level Models from RTL Designs for Processors and Accelerators. DATE Yu Zeng, Aarti Gupta, Sharad Malik
2022	A	`conf`	Compositional Verification Using a Formal Component and Interface Specification. ICCAD Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik
2022	B	`conf`	Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. FMCAD Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh
2022	—	`conf`	Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models. ASP-DAC Yue Xing, Aarti Gupta, Sharad Malik
2022	J	`jnl`	High-Level Synthesis for Packet-Processing Pipelines. CoRR Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta
2022	Misc	`conf`	Katra: Realtime Verification for Multilayer Networks. NSDI Ryan Beckett, Aarti Gupta
2022	B	`conf`	Kirigami, the Verifiable Art of Network Cutting. ICNP Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker
2022	J	`jnl`	Kirigami, the Verifiable Art of Network Cutting. CoRR Tim Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker
2022	J	`jnl`	Modular Control Plane Verification via Temporal Invariants. CoRR Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker
2022	J	`jnl`	Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface. CoRR Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Thierry Tambe, Gus Henry Smith, Akash Gaonkar, Vishal Canumalla, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik
2022	A	`conf`	Usage-Based RTL Subsetting for Hardware Accelerators. ICCAD Qinhan Tan, Aarti Gupta, Sharad Malik
2021	A	`conf`	Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables. ICCAD Yu Zeng, Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik
2021	A	`conf`	Leveraging Processor Modeling and Verification for General Hardware Modules. DATE Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik
2021	—	`conf`	Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett
2021	B	`conf`	Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. VMCAI Hongce Zhang, Aarti Gupta, Sharad Malik
2021	B	`conf`	Unbounded Procedure Summaries from Bounded Environments. VMCAI Lauren Pick, Grigory Fedyukovich, Aarti Gupta
2020	J	`jnl`	Abstract interpretation of distributed network control planes. Proc. ACM Program. Lang. Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
2020	B	`conf`	Automating Modular Verification of Secure Information Flow. FMCAD Lauren Pick, Grigory Fedyukovich, Aarti Gupta
2020	—	`conf`	Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
2020	A*	`conf`	In Search for a SAT-friendly Binarized Neural Network Architecture. ICLR Nina Narodytska, Hongce Zhang, Aarti Gupta, Toby Walsh
2020	A*	`conf`	Switch Code Generation Using Program Synthesis. SIGCOMM Xiangyu Gao, Taegyun Kim, Michael D. Wong, Divya Raghunathan, Aatish Kishan Varma, Pravein Govindan Kannan, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta
2020	B	`conf`	Synthesizing Environment Invariants for Modular Hardware Verification. VMCAI Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik
2020	A	`conf`	Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. ECAI Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska
2019	A	`conf`	FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. EuroSys Jeffrey F. Lukman, Huan Ke, Cesar A. Stuardo, Riza O. Suminto, Daniar Heri Kurniawan, Dikaimin Simon, Satria Priambada, Chen Tian, Feng Ye, Tanakorn Leesatapornwongsa, Aarti Gupta, Shan Lu, Haryadi S. Gunawi
2019	A	`conf`	Functional Synthesis with Examples. CP Grigory Fedyukovich, Aarti Gupta
2019	—	`conf`	ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions. TACAS (1) Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik
2019	J	`jnl`	Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. ACM Trans. Design Autom. Electr. Syst. Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik
2019	B	`conf`	Lazy but Effective Functional Synthesis. VMCAI Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
2019	A	`conf`	Lemma Synthesis for Automating Induction over Algebraic Data Types. CP Weikun Yang, Grigory Fedyukovich, Aarti Gupta
2019	—	`conf`	Quantified Invariants via Syntax-Guided Synthesis. CAV (1) Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
2018	A	`conf`	A formal instruction-level GPU model for scalable verification. ICCAD Yue Xing, Bo-Yuan Huang, Aarti Gupta, Sharad Malik
2018	J	`jnl`	Control Plane Compression. CoRR Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
2018	A*	`conf`	Control plane compression. SIGCOMM Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
2018	—	`conf`	Exploiting Synchrony and Symmetry in Relational Verification. CAV (1) Lauren Pick, Grigory Fedyukovich, Aarti Gupta
2018	A*	`conf`	Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. DAC Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik
2018	B	`conf`	ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. FMCAD Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, Sharad Malik
2018	J	`jnl`	Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. CoRR Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik
2018	—	`conf`	Lazy Self-composition for Security Verification. CAV (2) Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik
2018	—	`ch.`	Model Checking Concurrent Programs. Handbook of Model Checking Aarti Gupta, Vineet Kahlon, Shaz Qadeer, Tayssir Touili
2018	A*	`conf`	PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. MICRO Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Aarti Gupta
2018	B	`conf`	Solving Constrained Horn Clauses Using Syntax and Data. FMCAD Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
2018	—	`conf`	Syntax-Guided Termination Analysis. CAV (1) Grigory Fedyukovich, Yueling Zhang, Aarti Gupta
2018	J	`jnl`	Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, Sharad Malik
2017	A*	`conf`	A General Approach to Network Configuration Verification. SIGCOMM Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
2017	—	`conf`	Trace-based Analysis of Memory Corruption Malware Attacks. Haifa Verification Conference Zhixing Xu, Aarti Gupta, Sharad Malik
2016	B	`conf`	Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. SAS David Menendez, Santosh Nagarakatte, Aarti Gupta
2016	—	`conf`	Parallel data race detection for task parallel programs with locks. SIGSOFT FSE Adarsh Yoga, Santosh Nagarakatte, Aarti Gupta
2015	—	`conf`	Assertion guided symbolic execution of multithreaded programs. ESEC/SIGSOFT FSE Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, Aarti Gupta
2015	Misc	`conf`	Completeness bounds and sequentialization for model checking of interacting firmware and hardware. CODES+ISSS Sunha Ahn, Sharad Malik, Aarti Gupta
2015	J	`jnl`	Scalable and scope-bounded software verification in Varvel. Autom. Softw. Eng. Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Takashi Imoto, Rakesh Pothengil, Mustafa Hussain
2014	A	`conf`	ARC++: effective typestate and lifetime dependency analysis. ISSTA Xusheng Xiao, Gogul Balakrishnan, Franjo Ivancic, Naoto Maeda, Aarti Gupta, Deepak Chhetri
2014	A	`conf`	An Adaptable Rule Placement for Software-Defined Networks. DSN Shuyuan Zhang, Franjo Ivancic, Cristian Lumezanu, Yifei Yuan, Aarti Gupta, Sharad Malik
2014	—	`conf`	Environment-Sensitive Performance Tuning for Distributed Service Orchestration. VECPAR Yu Lin, Franjo Ivancic, Pallavi Joshi, Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta
2014	B	`conf`	Formally Verifying Graphics FPU - An Intel® Experience. FM Aarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal
2014	—	`conf`	Generating consistent updates for software-defined network configurations. HotSDN Yifei Yuan, Franjo Ivancic, Cristian Lumezanu, Shuyuan Zhang, Aarti Gupta
2014	—	`conf`	RTL2RTL Formal Equivalence: Boosting the Design Confidence. FSFMA M. V. Achutha Kiran Kumar, Aarti Gupta, S. S. Bindumadhava
2014	—	`conf`	ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs. SoCC Kaituo Li, Pallavi Joshi, Aarti Gupta, Malay K. Ganai
2013	A*	`conf`	Feedback-directed unit test generation for C/C++ using concolic execution. ICSE Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta
2013	J	`jnl`	Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. Houssam Abbas, Georgios Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
2013	—	`conf`	SETSUDŌ: perturbation-based testing framework for scalable distributed systems. TRIOS@SOSP Pallavi Joshi, Malay K. Ganai, Gogul Balakrishnan, Aarti Gupta, Nadia Papakonstantinou
2013	J	`jnl`	Static analysis for concurrent programs with applications to data race detection. Int. J. Softw. Tools Technol. Transf. Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta
2012	B	`conf`	Concurrent Test Generation Using Concolic Multi-trace Analysis. APLAS Niloofar Razavi, Franjo Ivancic, Vineet Kahlon, Aarti Gupta
2012	—	`conf`	DTAM: dynamic taint analysis of multi-threaded programs for relevancy. SIGSOFT FSE Malay K. Ganai, Dongyoon Lee, Aarti Gupta
2012	B	`conf`	Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. VMCAI Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta
2012	—	`conf`	Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. RP Khalil Ghorbal, Parasara Sridhar Duggirala, Vineet Kahlon, Franjo Ivancic, Aarti Gupta
2012	B	`conf`	Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. FMCAD Arnab Sinha, Sharad Malik, Aarti Gupta
2012	J	`jnl`	Introduction to special section on verification challenges in the concurrent world. ACM Trans. Design Autom. Electr. Syst. Sandip Ray, Jayanta Bhadra, Magdy S. Abadir, Li-C. Wang, Aarti Gupta
2012	B	`conf`	Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis. CC Jing Yang, Gogul Balakrishnan, Naoto Maeda, Franjo Ivancic, Aarti Gupta, Nishant Sinha, Sriram Sankaranarayanan, Naveen Sharma
2012	B	`conf`	Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPU. FMCAD V. M. Achutha KiranKumar, Aarti Gupta, Rajnish Ghughal
2011	A*	`conf`	BEST: A symbolic testing tool for predicting multi-threaded program failures. ASE Malay K. Ganai, Nipun Arora, Chao Wang, Aarti Gupta, Gogul Balakrishnan
2011	A*	`conf`	Coverage guided systematic concurrency testing. ICSE Chao Wang, Mahmoud Said, Aarti Gupta
2011	A*	`conf`	DC2: A framework for scalable, scope-bounded software verification. ASE Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Hiroki Tokuoka, Takashi Imoto, Yoshiaki Miyazaki
2011	A	`conf`	Interprocedural Exception Analysis for C++. ECOOP Prakash Prabhu, Naoto Maeda, Gogul Balakrishnan, Franjo Ivancic, Aarti Gupta
2011	—	`conf`	Modeling and Analyzing the Interaction of C and C++ Strings. FoVeOOS Gogul Balakrishnan, Naoto Maeda, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta, Rakesh Pothengil
2011	—	`conf`	Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search. Haifa Verification Conference Arnab Sinha, Sharad Malik, Chao Wang, Aarti Gupta
2011	C	`conf`	Predictive analysis for detecting serializability violations through Trace Segmentation. MEMOCODE Arnab Sinha, Sharad Malik, Chao Wang, Aarti Gupta
2011	J	`jnl`	Symbolic predictive analysis for concurrent programs. Formal Aspects Comput. Chao Wang, Sudipta Kundu, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta
2011	B	`conf`	Verifying concurrent programs: FMCAD Aarti Gupta
2010	B	`conf`	Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. FMCAD Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke
2010	—	`conf`	Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. HSCC Truong Nghiem, Sriram Sankaranarayanan, Georgios Fainekos, Franjo Ivancic, Aarti Gupta, George J. Pappas
2010	C	`conf`	Numerical stability analysis of floating-point computations using software model checking. MEMOCODE Franjo Ivancic, Malay K. Ganai, Sriram Sankaranarayanan, Aarti Gupta
2010	A*	`conf`	Program analysis via satisfiability modulo path programs. POPL William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
2010	B	`conf`	Scalable and precise program analysis at NEC. FMCAD Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang
2010	A	`conf`	Trace-Based Symbolic Analysis for Atomicity Violations. TACAS Chao Wang, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta
2009	B	`conf`	Model Checking Concurrent Programs. VMCAI Aarti Gupta
2009	J	`jnl`	Model checking sequential software programs via mixed symbolic analysis. ACM Trans. Design Autom. Electr. Syst. Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic
2009	A*	`conf`	Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. CAV Vineet Kahlon, Chao Wang, Aarti Gupta
2009	J	`jnl`	Preface. Formal Methods Syst. Des. Aarti Gupta, Sharad Malik
2009	Misc	`conf`	Refining the control structure of loops using static analysis. EMSOFT Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
2009	A	`conf`	Robustness of Model-Based Simulations. RTSS Georgios Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
2009	A	`conf`	Semantic Reduction of Thread Interleavings in Concurrent Programs. TACAS Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta
2009	B	`conf`	Symbolic Predictive Analysis for Concurrent Programs. FM Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta
2009	—	`conf`	Symbolic pruning of concurrent program executions. ESEC/SIGSOFT FSE Chao Wang, Swarat Chaudhuri, Aarti Gupta, Yu Yang
2008	J	`jnl`	Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivancic, Srihari Cadambi, Malay K. Ganai, Aarti Gupta, Pranav Ashar
2008	A	`conf`	Completeness in SMT-based BMC for Software Programs. DATE Malay K. Ganai, Aarti Gupta
2008	A*	`ed.`	Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings CAV Aarti Gupta, Sharad Malik
2008	B	`conf`	Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. ATVA Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan
2008	A	`conf`	Dynamic inference of likely data preconditions over predicates by tree learning. ISSTA Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, Aarti Gupta
2008	—	`conf`	Efficient Modeling of Concurrent Systems in BMC. SPIN Malay K. Ganai, Aarti Gupta
2008	J	`jnl`	Efficient SAT-based bounded model checking for software verification. Theor. Comput. Sci. Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Pranav Ashar
2008	A*	`conf`	Mining library specifications using inductive logic programming. ICSE Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
2008	—	`conf`	Modular verification of web services using efficient symbolic encoding and summarization. SIGSOFT FSE Fang Yu, Chao Wang, Aarti Gupta, Tevfik Bultan
2008	A	`conf`	Peephole Partial Order Reduction. TACAS Chao Wang, Zijiang Yang, Vineet Kahlon, Aarti Gupta
2008	B	`conf`	SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement. SAS Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Ou Wei, Aarti Gupta
2008	A	`conf`	Software Verification: Roles and Challenges for Automatic Decision Procedures. IJCAR Aarti Gupta
2008	A*	`conf`	Tunneling and slicing: towards scalable BMC. DAC Malay K. Ganai, Aarti Gupta
2007	J	`jnl`	Disjunctive image computation for software verification. ACM Trans. Design Autom. Electr. Syst. Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta
2007	—	`conf`	Efficient BMC for Multi-Clock Systems with Clocked Specifications. ASP-DAC Malay K. Ganai, Aarti Gupta
2007	A*	`conf`	Fast and Accurate Static Data-Race Detection for Concurrent Programs. CAV Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta
2007	—	`conf`	From Hardware Verification to Software Verification: Re-use and Re-learn. Haifa Verification Conference Aarti Gupta
2007	A	`conf`	Hybrid CEGAR: combining variable hiding and predicate abstraction. ICCAD Chao Wang, Hyondeuk Kim, Aarti Gupta
2007	B	`conf`	Induction in CEGAR for Detecting Counterexamples. FMCAD Chao Wang, Aarti Gupta, Franjo Ivancic
2007	A*	`conf`	On the analysis of interacting pushdown systems. POPL Vineet Kahlon, Aarti Gupta
2007	B	`conf`	Program Analysis Using Symbolic Ranges. SAS Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
2007	—	`book`	SAT-Based Scalable Formal Verification Solutions Malay K. Ganai, Aarti Gupta
2007	J	`jnl`	SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic. J. Satisf. Boolean Model. Comput. Malay K. Ganai, Muralidhar Talupur, Aarti Gupta
2007	Misc	`conf`	Synthesizing "Verification Aware" Models: Why and How? VLSI Design Malay K. Ganai, Akira Mukaiyama, Aarti Gupta, Kazutoshi Wakabayashi
2007	A*	`conf`	Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. CAV Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic
2007	A*	`conf`	Using Ontologies and the Web to Learn Lexical Semantics. IJCAI Aarti Gupta, Tim Oates
2007	J	`jnl`	Verification of Embedded Memory Systems using Efficient Memory Modeling CoRR Malay K. Ganai, Aarti Gupta, Pranav Ashar
2006	A	`conf`	Accelerating high-level bounded model checking. ICCAD Malay K. Ganai, Aarti Gupta
2006	A*	`conf`	An Automata-Theoretic Approach for Model Checking Threads for LTL Propert. LICS Vineet Kahlon, Aarti Gupta
2006	A	`conf`	Disjunctive image computation for embedded software verification. DATE Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta
2006	J	`jnl`	Efficient distributed SAT and SAT-based distributed Bounded Model Checking. Int. J. Softw. Tools Technol. Transf. Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar
2006	C	`conf`	Mixed symbolic representations for model checking software programs. MEMOCODE Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic
2006	A*	`conf`	Predicate learning and selective theory deduction for a difference logic solver. DAC Chao Wang, Aarti Gupta, Malay K. Ganai
2006	—	`conf`	SAT-Based Verification Methods and Applications in Hardware Verification. SFM Aarti Gupta, Malay K. Ganai, Chao Wang
2006	B	`conf`	Static Analysis in Disjunctive Numerical Domains. SAS Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta
2006	A*	`conf`	Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. CAV Vineet Kahlon, Aarti Gupta, Nishant Sinha
2006	A*	`conf`	Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. CAV Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang
2006	B	`conf`	Whodunit? Causal Analysis for Counterexamples. ATVA Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta
2005	J	`jnl`	A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. Mukul R. Prasad, Armin Biere, Aarti Gupta
2005	A*	`conf`	Beyond safety: customized SAT-based model checking. DAC Malay K. Ganai, Aarti Gupta, Pranav Ashar
2005	B	`conf`	Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. LPAR Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta
2005	A*	`conf`	F-Soft: Software Verification Platform. CAV Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar
2005	Misc	`conf`	Lazy Constraints and SAT Heuristics for Proof-Based Abstraction. VLSI Design Aarti Gupta, Malay K. Ganai, Pranav Ashar
2005	A	`conf`	Localization and Register Sharing for Predicate Abstraction. TACAS Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai
2005	C	`conf`	Model Checking C Programs Using F-SOFT. ICCD Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta, Malay K. Ganai, Vineet Kahlon, Chao Wang, Zijiang Yang
2005	A*	`conf`	Reasoning About Threads Communicating via Locks. CAV Vineet Kahlon, Franjo Ivancic, Aarti Gupta
2005	A*	`conf`	Symmetry Reduction in SAT-Based Model Checking. CAV Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip
2005	—	`ch.`	Verification Languages. The Industrial Information Technology Handbook Aarti Gupta, Ali Alphan Bayazit, Yogesh S. Mahajan
2005	—	`ch.`	Verification Languages. Embedded Systems Handbook Aarti Gupta, Ali Alphan Bayazit, Yogesh S. Mahajan
2005	A	`conf`	Verification of Embedded Memory Systems using Efficient Memory Modeling. DATE Malay K. Ganai, Aarti Gupta, Pranav Ashar
2004	A*	`conf`	Efficient Modeling of Embedded Memories in Bounded Model Checking. CAV Malay K. Ganai, Aarti Gupta, Pranav Ashar
2004	—	`conf`	Efficient SAT-based Bounded Model Checking for Software Verification. ISoLA (Preliminary proceedings) Pranav Ashar, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Zijiang Yang
2004	A	`conf`	Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. ICCAD Malay K. Ganai, Aarti Gupta, Pranav Ashar
2003	A*	`conf`	Abstraction and BDDs Complement SAT-Based BMC in DiVer. CAV Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar
2003	—	`conf`	Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking. CHARME Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar
2003	A	`conf`	Iterative Abstraction using SAT-based BMC with Proof Analysis. ICCAD Aarti Gupta, Malay K. Ganai, Zijiang Yang, Pranav Ashar
2003	A*	`conf`	Learning from BDDs in SAT-based bounded model checking. DAC Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar
2002	J	`jnl`	Assertion-based verification turns the corner. IEEE Des. Test Comput. Aarti Gupta
2002	A*	`conf`	Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. DAC Malay K. Ganai, Pranav Ashar, Aarti Gupta, Lintao Zhang, Sharad Malik
2002	—	`conf`	Property-Specific Testbench Generation for Guided Simulation. ASP-DAC/VLSI Design Aarti Gupta, Albert E. Casavant, Pranav Ashar, Sean Liu, Akira Mukaiyama, Kazutoshi Wakabayashi
2001	A*	`conf`	Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. DAC Aarti Gupta, Anubhav Gupta, Zijiang Yang, Pranav Ashar
2001	A	`conf`	Partition-Based Decision Heuristics for Image Computation Using SAT and BDDs. ICCAD Aarti Gupta, Zijiang Yang, Pranav Ashar, Lintao Zhang, Sharad Malik
2001	A	`conf`	Property-specific witness graph generation for guided simulation. DATE Albert E. Casavant, Aarti Gupta, S. Liu, Akira Mukaiyama, Kazutoshi Wakabayashi, Pranav Ashar
2001	J	`jnl`	Using complete-1-distinguishability for FSM equivalence checking. ACM Trans. Design Autom. Electr. Syst. Pranav Ashar, Aarti Gupta, Sharad Malik
2000	Misc	`conf`	Fast Error Diagnosis for Combinational Verification. VLSI Design Aarti Gupta, Pranav Ashar
2000	B	`conf`	SAT-Based Image Computation with Application in Reachability Analysis. FMCAD Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta
1999	—	`conf`	Exploiting Retiming in a Guided Simulation Based Validation Methodology. CHARME Aarti Gupta, Pranav Ashar, Sharad Malik
1999	C	`conf`	Verification of Scheduling in the Presence of Loops Using Uninterpreted Symbolic Simulation. ICCD Pranav Ashar, Anand Raghunathan, Aarti Gupta, Subhrajit Bhattacharya
1998	Misc	`conf`	Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking. VLSI Design Aarti Gupta, Pranav Ashar
1997	A*	`conf`	Toward Formalizing a Validation Methodology Using Simulation Coverage. DAC Aarti Gupta, Sharad Malik, Pranav Ashar
1996	A	`conf`	Using complete-1-distinguishability for FSM equivalence checking. ICCAD Pranav Ashar, Aarti Gupta, Sharad Malik
1994	C	`conf`	Tradeoffs in Canonical Sequential Function Representations. ICCD Aarti Gupta, Allan L. Fisher
1993	A*	`conf`	Parametric Circuit Representation Using Inductive Boolean Functions. CAV Aarti Gupta, Allan L. Fisher
1993	A	`conf`	Representation and symbolic manipulation of linearly inductive Boolean functions. ICCAD Aarti Gupta, Allan L. Fisher
1992	J	`jnl`	Formal Hardware Verification Methods: A Survey. Formal Methods Syst. Des. Aarti Gupta
1990	—	`conf`	Flexible Parallel Polygon Rendering. ICPP (3) Aarti Gupta, Allan L. Fisher
1986	—	`conf`	A Parallel Computer Based on Cube-Connected Cycles for Wafer-Scale. FJCC Moon-Jung Chung, Edward J. Toy, Aarti Gupta