![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
Aarti Gupta
Person information
- affiliation: Princeton University, NJ, USA
- affiliation (former): NEC Labs America, USA
Refine list
![note](https://dblp.dagstuhl.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j25]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
:
Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. ACM Trans. Design Autom. Electr. Syst. 29(2): 35:1-35:25 (2024) - [j24]Timothy Alberdingk Thijm
, Ryan Beckett, Aarti Gupta, David Walker:
Kirigami, the Verifiable Art of Network Cutting. IEEE/ACM Trans. Netw. 32(3): 2447-2462 (2024) - [c147]Yi Li, Aarti Gupta, Sharad Malik:
Exact Scheduling to Minimize Off-Chip Data Movement for Deep Learning Accelerators. ASPDAC 2024: 908-914 - [c146]Fengchen Gong
, Divya Raghunathan
, Aarti Gupta
, Maria Apostolaki
:
Zoom2Net: Constrained Network Telemetry Imputation. SIGCOMM 2024: 764-777 - [i10]Fengchen Gong, Divya Raghunathan, Aarti Gupta, Maria Apostolaki:
Super-resolution on network telemetry time series. CoRR abs/2403.04165 (2024) - 2023
- [j23]Timothy Alberdingk Thijm
, Ryan Beckett
, Aarti Gupta
, David Walker
:
Modular Control Plane Verification via Temporal Invariants. Proc. ACM Program. Lang. 7(PLDI): 50-75 (2023) - [j22]Lauren Pick
, Ankush Desai
, Aarti Gupta
:
Psym: Efficient Symbolic Exploration of Distributed Systems. Proc. ACM Program. Lang. 7(PLDI): 660-685 (2023) - [j21]Jingbo Wang
, Aarti Gupta
, Chao Wang
:
Synthesizing MILP Constraints for Efficient and Robust Optimization. Proc. ACM Program. Lang. 7(PLDI): 1896-1919 (2023) - [j20]Huaixi Lu
, Yue Xing
, Aarti Gupta
, Sharad Malik
:
SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications. ACM Trans. Design Autom. Electr. Syst. 28(6): 89:1-89:24 (2023) - [c145]Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta
:
CaT: A Solver-Aided Compiler for Packet-Processing Pipelines. ASPLOS (3) 2023: 72-88 - [c144]Bo-Yuan Huang, Hongce Zhang
, Aarti Gupta, Sharad Malik:
INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms. DAC 2023: 1-4 - [c143]Fengchen Gong
, Divya Raghunathan
, Aarti Gupta
, Maria Apostolaki
:
Towards Integrating Formal Methods into ML-Based Systems for Networking. HotNets 2023: 48-55 - [i9]Yi Li, Aarti Gupta, Sharad Malik:
Combined Scheduling, Memory Allocation and Tensor Replacement for Minimizing Off-Chip Data Accesses of DNN Accelerators. CoRR abs/2311.18246 (2023) - 2022
- [c142]Yue Xing, Aarti Gupta
, Sharad Malik
:
Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models. ASP-DAC 2022: 154-159 - [c141]Yu Zeng, Aarti Gupta
, Sharad Malik
:
Automatic Generation of Architecture-Level Models from RTL Designs for Processors and Accelerators. DATE 2022: 460-465 - [c140]Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh:
Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. FMCAD 2022: 151-159 - [c139]Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker:
ACORN: Network Control Plane Abstraction using Route Nondeterminism. FMCAD 2022: 261-272 - [c138]Yue Xing, Huaixi Lu, Aarti Gupta
, Sharad Malik
:
Compositional Verification Using a Formal Component and Interface Specification. ICCAD 2022: 72:1-72:9 - [c137]Qinhan Tan, Aarti Gupta
, Sharad Malik
:
Usage-Based RTL Subsetting for Hardware Accelerators. ICCAD 2022: 73:1-73:9 - [c136]Timothy Alberdingk Thijm
, Ryan Beckett, Aarti Gupta
, David Walker
:
Kirigami, the Verifiable Art of Network Cutting. ICNP 2022: 1-12 - [c135]Ryan Beckett, Aarti Gupta
:
Katra: Realtime Verification for Multilayer Networks. NSDI 2022: 617-634 - [i8]Tim Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker:
Kirigami, the Verifiable Art of Network Cutting. CoRR abs/2202.06098 (2022) - [i7]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
:
Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface. CoRR abs/2203.00218 (2022) - [i6]Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker
:
Modular Control Plane Verification via Temporal Invariants. CoRR abs/2204.10303 (2022) - [i5]Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker
:
ACORN: Network Control Plane Abstraction using Route Nondeterminism. CoRR abs/2206.02100 (2022) - [i4]Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta:
High-Level Synthesis for Packet-Processing Pipelines. CoRR abs/2211.06475 (2022) - 2021
- [c134]Makai Mann
, Ahmed Irfan
, Florian Lonsing
, Yahan Yang, Hongce Zhang
, Kristopher Brown
, Aarti Gupta
, Clark W. Barrett
:
Pono: A Flexible and Extensible SMT-Based Model Checker. CAV (2) 2021: 461-474 - [c133]Yue Xing, Huaixi Lu, Aarti Gupta
, Sharad Malik
:
Leveraging Processor Modeling and Verification for General Hardware Modules. DATE 2021: 1130-1135 - [c132]Yu Zeng, Bo-Yuan Huang
, Hongce Zhang
, Aarti Gupta
, Sharad Malik
:
Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables. ICCAD 2021: 1-9 - [c131]Lauren Pick, Grigory Fedyukovich
, Aarti Gupta
:
Unbounded Procedure Summaries from Bounded Environments. VMCAI 2021: 291-324 - [c130]Hongce Zhang
, Aarti Gupta, Sharad Malik:
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. VMCAI 2021: 325-349 - 2020
- [j19]Ryan Beckett, Aarti Gupta
, Ratul Mahajan, David Walker
:
Abstract interpretation of distributed network control planes. Proc. ACM Program. Lang. 4(POPL): 42:1-42:27 (2020) - [c129]Hongce Zhang
, Maxwell Shinn, Aarti Gupta
, Arie Gurfinkel
, Nham Le, Nina Narodytska:
Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. ECAI 2020: 1690-1697 - [c128]Lauren Pick, Grigory Fedyukovich, Aarti Gupta:
Automating Modular Verification of Secure Information Flow. FMCAD 2020: 158-168 - [c127]Nina Narodytska, Hongce Zhang
, Aarti Gupta
, Toby Walsh:
In Search for a SAT-friendly Binarized Neural Network Architecture. ICLR 2020 - [c126]Xiangyu Gao, Taegyun Kim, Michael D. Wong, Divya Raghunathan, Aatish Kishan Varma, Pravein Govindan Kannan
, Anirudh Sivaraman, Srinivas Narayana, Aarti Gupta
:
Switch Code Generation Using Program Synthesis. SIGCOMM 2020: 44-61 - [c125]Naoki Kobayashi
, Grigory Fedyukovich
, Aarti Gupta
:
Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) 2020: 195-214 - [c124]Hongce Zhang
, Weikun Yang, Grigory Fedyukovich
, Aarti Gupta, Sharad Malik:
Synthesizing Environment Invariants for Modular Hardware Verification. VMCAI 2020: 202-225
2010 – 2019
- 2019
- [j18]Bo-Yuan Huang
, Hongce Zhang
, Pramod Subramanyan, Yakir Vizel, Aarti Gupta
, Sharad Malik
:
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. ACM Trans. Design Autom. Electr. Syst. 24(1): 10:1-10:24 (2019) - [c123]Grigory Fedyukovich
, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta:
Quantified Invariants via Syntax-Guided Synthesis. CAV (1) 2019: 259-277 - [c122]Grigory Fedyukovich
, Aarti Gupta:
Functional Synthesis with Examples. CP 2019: 547-564 - [c121]Weikun Yang, Grigory Fedyukovich
, Aarti Gupta:
Lemma Synthesis for Automating Induction over Algebraic Data Types. CP 2019: 600-617 - [c120]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:
FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. EuroSys 2019: 20:1-20:16 - [c119]Bo-Yuan Huang, Hongce Zhang
, Aarti Gupta, Sharad Malik:
ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions. TACAS (1) 2019: 351-357 - [c118]Grigory Fedyukovich
, Arie Gurfinkel
, Aarti Gupta:
Lazy but Effective Functional Synthesis. VMCAI 2019: 92-113 - 2018
- [j17]Pramod Subramanyan
, Bo-Yuan Huang
, Yakir Vizel, Aarti Gupta
, Sharad Malik
:
Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(8): 1692-1705 (2018) - [c117]Grigory Fedyukovich
, Yueling Zhang, Aarti Gupta:
Syntax-Guided Termination Analysis. CAV (1) 2018: 124-143 - [c116]Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik:
Lazy Self-composition for Security Verification. CAV (2) 2018: 136-156 - [c115]Lauren Pick, Grigory Fedyukovich
, Aarti Gupta:
Exploiting Synchrony and Symmetry in Relational Verification. CAV (1) 2018: 164-182 - [c114]Bo-Yuan Huang
, Sayak Ray, Aarti Gupta
, Jason M. Fung, Sharad Malik
:
Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. DAC 2018: 91:1-91:6 - [c113]Grigory Fedyukovich
, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta
:
Solving Constrained Horn Clauses Using Syntax and Data. FMCAD 2018: 1-9 - [c112]Hongce Zhang
, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta
, Margaret Martonosi, Sharad Malik
:
ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. FMCAD 2018: 1-10 - [c111]Yue Xing, Bo-Yuan Huang
, Aarti Gupta
, Sharad Malik
:
A formal instruction-level GPU model for scalable verification. ICCAD 2018: 130 - [c110]Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Aarti Gupta
:
PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. MICRO 2018: 788-801 - [c109]Ryan Beckett, Aarti Gupta
, Ratul Mahajan, David Walker
:
Control plane compression. SIGCOMM 2018: 476-489 - [p2]Aarti Gupta, Vineet Kahlon, Shaz Qadeer, Tayssir Touili:
Model Checking Concurrent Programs. Handbook of Model Checking 2018: 573-611 - [i3]Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, Sharad Malik:
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. CoRR abs/1801.01114 (2018) - [i2]Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker:
Control Plane Compression. CoRR abs/1806.08744 (2018) - 2017
- [c108]Zhixing Xu, Aarti Gupta, Sharad Malik:
Trace-based Analysis of Memory Corruption Malware Attacks. Haifa Verification Conference 2017: 67-82 - [c107]Ryan Beckett, Aarti Gupta
, Ratul Mahajan, David Walker
:
A General Approach to Network Configuration Verification. SIGCOMM 2017: 155-168 - 2016
- [c106]David Menendez, Santosh Nagarakatte
, Aarti Gupta:
Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. SAS 2016: 317-337 - [c105]Adarsh Yoga, Santosh Nagarakatte
, Aarti Gupta
:
Parallel data race detection for task parallel programs with locks. SIGSOFT FSE 2016: 833-845 - 2015
- [j16]Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta
, Sriram Sankaranarayanan, Naoto Maeda, Takashi Imoto, Rakesh Pothengil, Mustafa Hussain:
Scalable and scope-bounded software verification in Varvel. Autom. Softw. Eng. 22(4): 517-559 (2015) - [c104]Sunha Ahn, Sharad Malik
, Aarti Gupta
:
Completeness bounds and sequentialization for model checking of interacting firmware and hardware. CODES+ISSS 2015: 202-211 - [c103]Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, Aarti Gupta
:
Assertion guided symbolic execution of multithreaded programs. ESEC/SIGSOFT FSE 2015: 854-865 - 2014
- [c102]Kaituo Li, Pallavi Joshi, Aarti Gupta
, Malay K. Ganai:
ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs. SoCC 2014: 25:1-25:13 - [c101]Shuyuan Zhang, Franjo Ivancic, Cristian Lumezanu, Yifei Yuan, Aarti Gupta
, Sharad Malik
:
An Adaptable Rule Placement for Software-Defined Networks. DSN 2014: 88-99 - [c100]Aarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal:
Formally Verifying Graphics FPU - An Intel® Experience. FM 2014: 673-687 - [c99]Xusheng Xiao
, Gogul Balakrishnan, Franjo Ivancic, Naoto Maeda, Aarti Gupta
, Deepak Chhetri:
ARC++: effective typestate and lifetime dependency analysis. ISSTA 2014: 116-126 - [c98]Yifei Yuan, Franjo Ivancic, Cristian Lumezanu, Shuyuan Zhang, Aarti Gupta
:
Generating consistent updates for software-defined network configurations. HotSDN 2014: 221-222 - [c97]Yu Lin, Franjo Ivancic, Pallavi Joshi, Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta:
Environment-Sensitive Performance Tuning for Distributed Service Orchestration. VECPAR 2014: 209-223 - [c96]M. V. Achutha Kiran Kumar, Aarti Gupta, S. S. Bindumadhava:
RTL2RTL Formal Equivalence: Boosting the Design Confidence. FSFMA 2014: 29-44 - 2013
- [j15]Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta
:
Static analysis for concurrent programs with applications to data race detection. Int. J. Softw. Tools Technol. Transf. 15(4): 321-336 (2013) - [j14]Houssam Abbas, Georgios Fainekos
, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
:
Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 12(2s): 95:1-95:30 (2013) - [c95]Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta
:
Feedback-directed unit test generation for C/C++ using concolic execution. ICSE 2013: 132-141 - [c94]Pallavi Joshi, Malay K. Ganai, Gogul Balakrishnan, Aarti Gupta
, Nadia Papakonstantinou:
SETSUDŌ: perturbation-based testing framework for scalable distributed systems. TRIOS@SOSP 2013: 7:1-7:14 - 2012
- [j13]Sandip Ray, Jayanta Bhadra, Magdy S. Abadir, Li-C. Wang
, Aarti Gupta
:
Introduction to special section on verification challenges in the concurrent world. ACM Trans. Design Autom. Electr. Syst. 17(3): 19:1-19:3 (2012) - [c93]Niloofar Razavi, Franjo Ivancic, Vineet Kahlon, Aarti Gupta:
Concurrent Test Generation Using Concolic Multi-trace Analysis. APLAS 2012: 239-255 - [c92]Jing Yang, Gogul Balakrishnan, Naoto Maeda, Franjo Ivancic, Aarti Gupta, Nishant Sinha, Sriram Sankaranarayanan, Naveen Sharma:
Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis. CC 2012: 144-164 - [c91]Arnab Sinha, Sharad Malik
, Aarti Gupta
:
Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. FMCAD 2012: 6-15 - [c90]V. M. Achutha KiranKumar, Aarti Gupta, Rajnish Ghughal:
Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPU. FMCAD 2012: 149-156 - [c89]Khalil Ghorbal, Parasara Sridhar Duggirala, Vineet Kahlon, Franjo Ivancic, Aarti Gupta:
Efficient Probabilistic Model Checking of Systems with Ranged Probabilities. RP 2012: 107-120 - [c88]Malay K. Ganai, Dongyoon Lee
, Aarti Gupta
:
DTAM: dynamic taint analysis of multi-threaded programs for relevancy. SIGSOFT FSE 2012: 46 - [c87]Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta:
Donut Domains: Efficient Non-convex Domains for Abstract Interpretation. VMCAI 2012: 235-250 - 2011
- [j12]Chao Wang, Sudipta Kundu, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta
:
Symbolic predictive analysis for concurrent programs. Formal Aspects Comput. 23(6): 781-805 (2011) - [c86]Prakash Prabhu, Naoto Maeda, Gogul Balakrishnan, Franjo Ivancic, Aarti Gupta:
Interprocedural Exception Analysis for C++. ECOOP 2011: 583-608 - [c85]Aarti Gupta
:
Verifying concurrent programs: tutorial talk. FMCAD 2011: 1 - [c84]Gogul Balakrishnan, Naoto Maeda, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta, Rakesh Pothengil:
Modeling and Analyzing the Interaction of C and C++ Strings. FoVeOOS 2011: 67-85 - [c83]Arnab Sinha, Sharad Malik, Chao Wang, Aarti Gupta:
Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search. Haifa Verification Conference 2011: 95-114 - [c82]Chao Wang, Mahmoud Said, Aarti Gupta
:
Coverage guided systematic concurrency testing. ICSE 2011: 221-230 - [c81]Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta
, Sriram Sankaranarayanan, Naoto Maeda, Hiroki Tokuoka, Takashi Imoto, Yoshiaki Miyazaki:
DC2: A framework for scalable, scope-bounded software verification. ASE 2011: 133-142 - [c80]Malay K. Ganai, Nipun Arora, Chao Wang, Aarti Gupta
, Gogul Balakrishnan:
BEST: A symbolic testing tool for predicting multi-threaded program failures. ASE 2011: 596-599 - [c79]Arnab Sinha, Sharad Malik
, Chao Wang, Aarti Gupta
:
Predictive analysis for detecting serializability violations through Trace Segmentation. MEMOCODE 2011: 99-108 - 2010
- [c78]Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta
, Sriram Sankaranarayanan, Edmund M. Clarke:
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. FMCAD 2010: 81-89 - [c77]Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta
, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang:
Scalable and precise program analysis at NEC. FMCAD 2010: 273-274 - [c76]Truong Nghiem
, Sriram Sankaranarayanan, Georgios Fainekos
, Franjo Ivancic, Aarti Gupta
, George J. Pappas
:
Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. HSCC 2010: 211-220 - [c75]Franjo Ivancic, Malay K. Ganai, Sriram Sankaranarayanan, Aarti Gupta
:
Numerical stability analysis of floating-point computations using software model checking. MEMOCODE 2010: 49-58 - [c74]William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
:
Program analysis via satisfiability modulo path programs. POPL 2010: 71-82 - [c73]Chao Wang, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta:
Trace-Based Symbolic Analysis for Atomicity Violations. TACAS 2010: 328-342
2000 – 2009
- 2009
- [j11]Aarti Gupta
, Sharad Malik
:
Preface. Formal Methods Syst. Des. 35(1): 1 (2009) - [j10]Zijiang Yang, Chao Wang, Aarti Gupta
, Franjo Ivancic:
Model checking sequential software programs via mixed symbolic analysis. ACM Trans. Design Autom. Electr. Syst. 14(1): 10:1-10:26 (2009) - [c72]Vineet Kahlon, Chao Wang, Aarti Gupta:
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. CAV 2009: 398-413 - [c71]Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
:
Refining the control structure of loops using static analysis. EMSOFT 2009: 49-58 - [c70]Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta:
Symbolic Predictive Analysis for Concurrent Programs. FM 2009: 256-272 - [c69]Georgios Fainekos
, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
:
Robustness of Model-Based Simulations. RTSS 2009: 345-354 - [c68]Chao Wang, Swarat Chaudhuri, Aarti Gupta
, Yu Yang:
Symbolic pruning of concurrent program executions. ESEC/SIGSOFT FSE 2009: 23-32 - [c67]Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta:
Semantic Reduction of Thread Interleavings in Concurrent Programs. TACAS 2009: 124-138 - [c66]Aarti Gupta:
Model Checking Concurrent Programs. VMCAI 2009: 2 - 2008
- [j9]Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivancic, Srihari Cadambi, Malay K. Ganai, Aarti Gupta
, Pranav Ashar:
Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(8): 1513-1517 (2008) - [j8]Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta
, Pranav Ashar:
Efficient SAT-based bounded model checking for software verification. Theor. Comput. Sci. 404(3): 256-274 (2008) - [c65]Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan:
Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. ATVA 2008: 126-140 - [c64]Aarti Gupta:
Software Verification: Roles and Challenges for Automatic Decision Procedures. IJCAR 2008: 1 - [c63]Malay K. Ganai, Aarti Gupta
:
Tunneling and slicing: towards scalable BMC. DAC 2008: 137-142 - [c62]Malay K. Ganai, Aarti Gupta
:
Completeness in SMT-based BMC for Software Programs. DATE 2008: 831-836 - [c61]Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta
:
Mining library specifications using inductive logic programming. ICSE 2008: 131-140 - [c60]Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, Aarti Gupta
:
Dynamic inference of likely data preconditions over predicates by tree learning. ISSTA 2008: 295-306 - [c59]Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Ou Wei, Aarti Gupta:
SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement. SAS 2008: 238-254 - [c58]Fang Yu, Chao Wang, Aarti Gupta
, Tevfik Bultan:
Modular verification of web services using efficient symbolic encoding and summarization. SIGSOFT FSE 2008: 192-202 - [c57]Malay K. Ganai, Aarti Gupta:
Efficient Modeling of Concurrent Systems in BMC. SPIN 2008: 114-133 - [c56]Chao Wang, Zijiang Yang, Vineet Kahlon, Aarti Gupta:
Peephole Partial Order Reduction. TACAS 2008: 382-396 - [e1]Aarti Gupta
, Sharad Malik
:
Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings. Lecture Notes in Computer Science 5123, Springer 2008, ISBN 978-3-540-70543-7 [contents] - 2007
- [b1]Malay K. Ganai, Aarti Gupta
:
SAT-Based Scalable Formal Verification Solutions. Series on Integrated Circuits and Systems, Springer 2007, ISBN 978-0-387-69166-4, pp. 1-326 - [j7]Malay K. Ganai, Muralidhar Talupur, Aarti Gupta
:
SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic. J. Satisf. Boolean Model. Comput. 3(1-2): 91-114 (2007) - [j6]Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta
:
Disjunctive image computation for software verification. ACM Trans. Design Autom. Electr. Syst. 12(2): 10 (2007) - [c55]Malay K. Ganai, Aarti Gupta
:
Efficient BMC for Multi-Clock Systems with Clocked Specifications. ASP-DAC 2007: 310-315 - [c54]Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta:
Fast and Accurate Static Data-Race Detection for Concurrent Programs. CAV 2007: 226-239 - [c53]Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic:
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. CAV 2007: 352-365 - [c52]Chao Wang, Aarti Gupta
, Franjo Ivancic:
Induction in CEGAR for Detecting Counterexamples. FMCAD 2007: 77-84 - [c51]Aarti Gupta:
From Hardware Verification to Software Verification: Re-use and Re-learn. Haifa Verification Conference 2007: 14-15 - [c50]Chao Wang, Hyondeuk Kim, Aarti Gupta
:
Hybrid CEGAR: combining variable hiding and predicate abstraction. ICCAD 2007: 310-317 - [c49]Aarti Gupta, Tim Oates:
Using Ontologies and the Web to Learn Lexical Semantics. IJCAI 2007: 1618-1623 - [c48]Vineet Kahlon, Aarti Gupta
:
On the analysis of interacting pushdown systems. POPL 2007: 303-314 - [c47]Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta:
Program Analysis Using Symbolic Ranges. SAS 2007: 366-383 - [c46]Malay K. Ganai, Akira Mukaiyama, Aarti Gupta
, Kazutoshi Wakabayashi:
Synthesizing "Verification Aware" Models: Why and How? VLSI Design 2007: 50-56 - [i1]Malay K. Ganai, Aarti Gupta, Pranav Ashar:
Verification of Embedded Memory Systems using Efficient Memory Modeling. CoRR abs/0710.4666 (2007) - 2006
- [j5]Malay K. Ganai, Aarti Gupta
, Zijiang Yang, Pranav Ashar:
Efficient distributed SAT and SAT-based distributed Bounded Model Checking. Int. J. Softw. Tools Technol. Transf. 8(4-5): 387-396 (2006) - [c45]Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta:
Whodunit? Causal Analysis for Counterexamples. ATVA 2006: 82-95 - [c44]Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang:
Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. CAV 2006: 137-151 - [c43]Vineet Kahlon, Aarti Gupta, Nishant Sinha:
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. CAV 2006: 286-299 - [c42]Chao Wang, Aarti Gupta
, Malay K. Ganai:
Predicate learning and selective theory deduction for a difference logic solver. DAC 2006: 235-240 - [c41]Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta
:
Disjunctive image computation for embedded software verification. DATE 2006: 1205-1210 - [c40]Malay K. Ganai, Aarti Gupta
:
Accelerating high-level bounded model checking. ICCAD 2006: 794-801 - [c39]Vineet Kahlon, Aarti Gupta
:
An Automata-Theoretic Approach for Model Checking Threads for LTL Propert. LICS 2006: 101-110 - [c38]Zijiang Yang, Chao Wang, Aarti Gupta
, Franjo Ivancic:
Mixed symbolic representations for model checking software programs. MEMOCODE 2006: 17-26 - [c37]Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta:
Static Analysis in Disjunctive Numerical Domains. SAS 2006: 3-17 - [c36]Aarti Gupta, Malay K. Ganai, Chao Wang:
SAT-Based Verification Methods and Applications in Hardware Verification. SFM 2006: 108-143 - [c35]Malay K. Ganai, Muralidhar Talupur, Aarti Gupta:
SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. TACAS 2006: 135-150 - 2005
- [j4]Mukul R. Prasad, Armin Biere
, Aarti Gupta
:
A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2): 156-173 (2005) - [c34]Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip:
Symmetry Reduction in SAT-Based Model Checking. CAV 2005: 125-138 - [c33]Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar:
F-Soft: Software Verification Platform. CAV 2005: 301-306 - [c32]Vineet Kahlon, Franjo Ivancic, Aarti Gupta:
Reasoning About Threads Communicating via Locks. CAV 2005: 505-518 - [c31]Malay K. Ganai, Aarti Gupta
, Pranav Ashar:
Beyond safety: customized SAT-based model checking. DAC 2005: 738-743 - [c30]Malay K. Ganai, Aarti Gupta
, Pranav Ashar:
Verification of Embedded Memory Systems using Efficient Memory Modeling. DATE 2005: 1096-1101 - [c29]Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta
, Malay K. Ganai, Vineet Kahlon, Chao Wang, Zijiang Yang:
Model Checking C Programs Using F-SOFT. ICCD 2005: 297-308 - [c28]Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta:
Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. LPAR 2005: 322-336 - [c27]Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai:
Localization and Register Sharing for Predicate Abstraction. TACAS 2005: 397-412 - [c26]Malay K. Ganai, Aarti Gupta, Pranav Ashar:
DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. TACAS 2005: 575-580 - [c25]Aarti Gupta
, Malay K. Ganai, Pranav Ashar:
Lazy Constraints and SAT Heuristics for Proof-Based Abstraction. VLSI Design 2005: 183-188 - [p1]Aarti Gupta, Ali Alphan Bayazit, Yogesh S. Mahajan:
Verification Languages. The Industrial Information Technology Handbook 2005: 1-18 - [r1]Aarti Gupta
, Ali Alphan Bayazit, Yogesh S. Mahajan:
Verification Languages. Embedded Systems Handbook 2005 - 2004
- [c24]Malay K. Ganai, Aarti Gupta, Pranav Ashar:
Efficient Modeling of Embedded Memories in Bounded Model Checking. CAV 2004: 440-452 - [c23]Malay K. Ganai, Aarti Gupta
, Pranav Ashar:
Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. ICCAD 2004: 510-517 - [c22]Pranav Ashar, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Zijiang Yang:
Efficient SAT-based Bounded Model Checking for Software Verification. ISoLA (Preliminary proceedings) 2004: 157-164 - 2003
- [c21]Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar:
Abstraction and BDDs Complement SAT-Based BMC in DiVer. CAV 2003: 206-209 - [c20]Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar:
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking. CHARME 2003: 334-347 - [c19]Aarti Gupta
, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar:
Learning from BDDs in SAT-based bounded model checking. DAC 2003: 824-829 - [c18]Aarti Gupta
, Malay K. Ganai, Zijiang Yang, Pranav Ashar:
Iterative Abstraction using SAT-based BMC with Proof Analysis. ICCAD 2003: 416-423 - 2002
- [j3]Aarti Gupta
:
Assertion-based verification turns the corner. IEEE Des. Test Comput. 19(4): 131-132 (2002) - [c17]Malay K. Ganai, Pranav Ashar, Aarti Gupta
, Lintao Zhang, Sharad Malik
:
Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. DAC 2002: 747-750 - [c16]Aarti Gupta
, Albert E. Casavant, Pranav Ashar, Sean Liu, Akira Mukaiyama, Kazutoshi Wakabayashi:
Property-Specific Testbench Generation for Guided Simulation. ASP-DAC/VLSI Design 2002: 524- - 2001
- [j2]Pranav Ashar, Aarti Gupta
, Sharad Malik
:
Using complete-1-distinguishability for FSM equivalence checking. ACM Trans. Design Autom. Electr. Syst. 6(4): 569-590 (2001) - [c15]Aarti Gupta
, Anubhav Gupta, Zijiang Yang, Pranav Ashar:
Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. DAC 2001: 536-541 - [c14]Albert E. Casavant, Aarti Gupta
, S. Liu, Akira Mukaiyama, Kazutoshi Wakabayashi, Pranav Ashar:
Property-specific witness graph generation for guided simulation. DATE 2001: 799 - [c13]Aarti Gupta
, Zijiang Yang, Pranav Ashar, Lintao Zhang, Sharad Malik
:
Partition-Based Decision Heuristics for Image Computation Using SAT and BDDs. ICCAD 2001: 286-292 - 2000
- [c12]Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav Gupta:
SAT-Based Image Computation with Application in Reachability Analysis. FMCAD 2000: 354-371 - [c11]Aarti Gupta
, Pranav Ashar:
Fast Error Diagnosis for Combinational Verification. VLSI Design 2000: 442-448
1990 – 1999
- 1999
- [c10]Aarti Gupta, Pranav Ashar, Sharad Malik:
Exploiting Retiming in a Guided Simulation Based Validation Methodology. CHARME 1999: 350-353 - [c9]Pranav Ashar, Anand Raghunathan, Aarti Gupta
, Subhrajit Bhattacharya:
Verification of Scheduling in the Presence of Loops Using Uninterpreted Symbolic Simulation. ICCD 1999: 458-466 - 1998
- [c8]Aarti Gupta
, Pranav Ashar:
Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking. VLSI Design 1998: 222-225 - 1997
- [c7]Aarti Gupta
, Sharad Malik
, Pranav Ashar:
Toward Formalizing a Validation Methodology Using Simulation Coverage. DAC 1997: 740-745 - 1996
- [c6]Pranav Ashar, Aarti Gupta
, Sharad Malik
:
Using complete-1-distinguishability for FSM equivalence checking. ICCAD 1996: 346-353 - 1994
- [c5]Aarti Gupta
, Allan L. Fisher:
Tradeoffs in Canonical Sequential Function Representations. ICCD 1994: 111-116 - 1993
- [c4]Aarti Gupta, Allan L. Fisher:
Parametric Circuit Representation Using Inductive Boolean Functions. CAV 1993: 15-28 - [c3]Aarti Gupta
, Allan L. Fisher:
Representation and symbolic manipulation of linearly inductive Boolean functions. ICCAD 1993: 192-199 - 1992
- [j1]Aarti Gupta
:
Formal Hardware Verification Methods: A Survey. Formal Methods Syst. Des. 1(2/3): 151-238 (1992) - 1990
- [c2]Aarti Gupta, Allan L. Fisher:
Flexible Parallel Polygon Rendering. ICPP (3) 1990: 87-91
1980 – 1989
- 1986
- [c1]Moon-Jung Chung, Edward J. Toy, Aarti Gupta:
A Parallel Computer Based on Cube-Connected Cycles for Wafer-Scale. FJCC 1986: 325-334
Coauthor Index
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-23 18:29 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint