BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × Austria
1 × Cyprus
1 × Denmark
1 × Estonia
1 × Greece
1 × Hungary
1 × Korea
1 × Singapore
2 × France
2 × Italy
2 × Spain
2 × The Netherlands
20 × USA
4 × United Kingdom
6 × Germany
Collaborated with:
M.K.Ganai C.Wang F.Ivancic P.Ashar V.Kahlon S.Sankaranarayanan Z.Yang G.Balakrishnan N.Maeda ∅ S.Malik G.Fedyukovich M.Talupur I.Shlyakhter S.Chaudhuri Y.Yang A.L.Fisher N.Sinha H.Jain V.M.A.KiranKumar R.Ghughal D.Lee M.Said A.Yoga S.Nagarakatte Y.Zhang L.Pick W.R.Harris R.Limaye S.Kundu F.Yu T.Bultan D.Tang C.N.Ip A.Gupta S.Prabhu K.Madhukar R.Beckett R.Mahajan D.Walker S.Guo M.Kusano P.Garg K.Ghorbal N.Arora P.Prabhu O.Wei L.Zhang W.Yang Y.Vizel P.Subramanyan X.Xiao D.Chhetri A.E.Casavant S.Liu A.Mukaiyama K.Wakabayashi J.Yang N.Sharma H.Tokuoka T.Imoto Y.Miyazaki
Talks about:
program (16) analysi (12) model (11) verif (10) base (10) use (10) symbol (9) check (8) sat (8) concurr (7)

Person: Aarti Gupta

DBLP DBLP: Gupta:Aarti

Facilitated 1 volumes:

CAV 2008Ed

Contributed to:

ESEC/FSE 20152015
FM 20142014
ISSTA 20142014
ICSE 20132013
CC 20122012
FSE 20122012
VMCAI 20122012
ASE 20112011
ECOOP 20112011
ICSE 20112011
POPL 20102010
TACAS 20102010
CAV 20092009
ESEC/FSE 20092009
FM 20092009
TACAS 20092009
VMCAI 20092009
DAC 20082008
DATE 20082008
FSE 20082008
ICSE 20082008
IJCAR 20082008
ISSTA 20082008
SAS 20082008
TACAS 20082008
CAV 20072007
POPL 20072007
SAS 20072007
CAV 20062006
DAC 20062006
DATE 20062006
LICS 20062006
SAS 20062006
SFM 20062006
TACAS 20062006
CAV 20052005
DAC 20052005
DATE 20052005
TACAS 20052005
CAV 20042004
CAV 20032003
DAC 20032003
DAC 20022002
DAC 20012001
DATE 20012001
DAC 19971997
CAV 19931993
FSE 20162016
CAV (1) 20182018
CAV (2) 20182018
CAV (1) 20192019
POPL 20202020
SMT 20062007

Wrote 61 papers:

ESEC-FSE-2015-GuoKWYG #execution #parallel #source code #symbolic computation #thread
Assertion guided symbolic execution of multithreaded programs (SG, MK, CW, ZY, AG), pp. 854–865.
FM-2014-GuptaKG #experience #verification
Formally Verifying Graphics FPU — An Intel® Experience (AG, VMAK, RG), pp. 673–687.
ISSTA-2014-XiaoBIMGC #analysis #dependence #effectiveness #type system
ARC++: effective typestate and lifetime dependency analysis (XX, GB, FI, NM, AG, DC), pp. 116–126.
ICSE-2013-GargIBMG #c #c++ #execution #generative #testing #using
Feedback-directed unit test generation for C/C++ using concolic execution (PG, FI, GB, NM, AG), pp. 132–141.
CC-2012-YangBMIGSSS #c++ #inheritance #program analysis
Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis (JY, GB, NM, FI, AG, NS, SS, NS), pp. 144–164.
FSE-2012-GanaiLG #analysis #concurrent #multi #named #source code #thread
DTAM: dynamic taint analysis of multi-threaded programs for relevancy (MKG, DL, AG), p. 46.
VMCAI-2012-GhorbalIBMG #abstract interpretation #performance
Donut Domains: Efficient Non-convex Domains for Abstract Interpretation (KG, FI, GB, NM, AG), pp. 235–250.
ASE-2011-GanaiAWGB #concurrent #multi #named #predict #testing #thread
BEST: A symbolic testing tool for predicting multi-threaded program failures (MKG, NA, CW, AG, GB), pp. 596–599.
ASE-2011-IvancicBGSMTIM #bound #framework #named #scalability #verification
DC2: A framework for scalable, scope-bounded software verification (FI, GB, AG, SS, NM, HT, TI, YM), pp. 133–142.
ECOOP-2011-PrabhuMBIG #analysis #c++ #exception #interprocedural
Interprocedural Exception Analysis for C++ (PP, NM, GB, FI, AG), pp. 583–608.
ICSE-2011-WangSG #concurrent #testing
Coverage guided systematic concurrency testing (CW, MS, AG), pp. 221–230.
POPL-2010-HarrisSIG #program analysis #satisfiability #source code
Program analysis via satisfiability modulo path programs (WRH, SS, FI, AG), pp. 71–82.
TACAS-2010-WangLGG #analysis
Trace-Based Symbolic Analysis for Atomicity Violations (CW, RL, MKG, AG), pp. 328–342.
CAV-2009-KahlonWG #partial order #reduction
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique (VK, CW, AG), pp. 398–413.
ESEC-FSE-2009-WangCGY #concurrent
Symbolic pruning of concurrent program executions (CW, SC, AG, YY), pp. 23–32.
FM-2009-WangKGG #analysis #concurrent #predict #source code
Symbolic Predictive Analysis for Concurrent Programs (CW, SK, MKG, AG), pp. 256–272.
TACAS-2009-KahlonSG #concurrent #reduction #semantics #source code #thread
Semantic Reduction of Thread Interleavings in Concurrent Programs (VK, SS, AG), pp. 124–138.
VMCAI-2009-Gupta #concurrent #model checking #source code
Model Checking Concurrent Programs (AG), p. 2.
DAC-2008-GanaiG #scalability #slicing #towards
Tunneling and slicing: towards scalable BMC (MKG, AG), pp. 137–142.
DATE-2008-GanaiG #smt #source code
Completeness in SMT-based BMC for Software Programs (MKG, AG), pp. 831–836.
FSE-2008-YuWGB #composition #encoding #performance #summary #using #verification #web #web service
Modular verification of web services using efficient symbolic encoding and summarization (FY, CW, AG, TB), pp. 192–202.
ICSE-2008-SankaranarayananIG #induction #library #logic programming #mining #specification #using
Mining library specifications using inductive logic programming (SS, FI, AG), pp. 131–140.
IJCAR-2008-Gupta #automation #challenge #verification
Software Verification: Roles and Challenges for Automatic Decision Procedures (AG), p. 1.
ISSTA-2008-SankaranarayananCIG #learning
Dynamic inference of likely data preconditions over predicates by tree learning (SS, SC, FI, AG), pp. 295–306.
SAS-2008-BalakrishnanSIWG #analysis #detection #named #refinement
SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement (GB, SS, FI, OW, AG), pp. 238–254.
TACAS-2008-WangYKG #partial order #reduction
Peephole Partial Order Reduction (CW, ZY, VK, AG), pp. 382–396.
CAV-2007-KahlonYSG #concurrent #detection #performance #source code
Fast and Accurate Static Data-Race Detection for Concurrent Programs (VK, YY, SS, AG), pp. 226–239.
CAV-2007-WangYGI #precise #reachability #using
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra (CW, ZY, AG, FI), pp. 352–365.
POPL-2007-KahlonG #analysis #automaton #on the
On the analysis of interacting pushdown systems (VK, AG), pp. 303–314.
SAS-2007-SankaranarayananIG #program analysis #using
Program Analysis Using Symbolic Ranges (SS, FI, AG), pp. 366–383.
CAV-2006-JainIGSW #abstraction #invariant #refinement #using
Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop (HJ, FI, AG, IS, CW), pp. 137–151.
CAV-2006-KahlonGS #concurrent #model checking #on the fly #partial order #source code #transaction #using
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions (VK, AG, NS), pp. 286–299.
DAC-2006-WangGG #deduction #difference #learning #logic
Predicate learning and selective theory deduction for a difference logic solver (CW, AG, MKG), pp. 235–240.
DATE-2006-WangYIG #embedded #image #verification
Disjunctive image computation for embedded software verification (CW, ZY, FI, AG), pp. 1205–1210.
LICS-2006-KahlonG #approach #ltl #model checking #thread
An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (VK, AG), pp. 101–110.
SAS-2006-SankaranarayananISG #static analysis
Static Analysis in Disjunctive Numerical Domains (SS, FI, IS, AG), pp. 3–17.
SFM-2006-GuptaGW #hardware #satisfiability #verification
SAT-Based Verification Methods and Applications in Hardware Verification (AG, MKG, CW), pp. 108–143.
TACAS-2006-GanaiTG #encoding #integration #lazy evaluation #logic #named
SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver (MKG, MT, AG), pp. 135–150.
CAV-2005-IvancicYGGSA #framework #named #platform #verification
F-Soft: Software Verification Platform (FI, ZY, MKG, AG, IS, PA), pp. 301–306.
CAV-2005-KahlonIG #communication #reasoning #thread
Reasoning About Threads Communicating via Locks (VK, FI, AG), pp. 505–518.
CAV-2005-TangMGI #model checking #reduction #satisfiability #symmetry
Symmetry Reduction in SAT-Based Model Checking (DT, SM, AG, CNI), pp. 125–138.
DAC-2005-GanaiGA #model checking #safety #satisfiability
Beyond safety: customized SAT-based model checking (MKG, AG, PA), pp. 738–743.
DATE-2005-GanaiGA #embedded #memory management #modelling #performance #using #verification
Verification of Embedded Memory Systems using Efficient Memory Modeling (MKG, AG, PA), pp. 1096–1101.
TACAS-2005-GanaiGA #framework #model checking #named #platform #satisfiability #scalability #verification
DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems (MKG, AG, PA), pp. 575–580.
TACAS-2005-JainIGG #abstraction #locality
Localization and Register Sharing for Predicate Abstraction (HJ, FI, AG, MKG), pp. 397–412.
CAV-2004-GanaiGA #bound #embedded #model checking #modelling #performance
Efficient Modeling of Embedded Memories in Bounded Model Checking (MKG, AG, PA), pp. 440–452.
CAV-2003-GuptaGWYA #abstraction #satisfiability
Abstraction and BDDs Complement SAT-Based BMC in DiVer (AG, MKG, CW, ZY, PA), pp. 206–209.
DAC-2003-GuptaGWYA #bound #learning #model checking #satisfiability
Learning from BDDs in SAT-based bounded model checking (AG, MKG, CW, ZY, PA), pp. 824–829.
DAC-2002-GanaiAGZM #algorithm #satisfiability
Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver (MKG, PA, AG, LZ, SM), pp. 747–750.
DAC-2001-GuptaGYA #detection #image #satisfiability
Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation (AG, AG, ZY, PA), pp. 536–541.
DATE-2001-CasavantGLMWA #generative #graph #simulation
Property-specific witness graph generation for guided simulation (AEC, AG, SL, AM, KW, PA), p. 799.
DAC-1997-GuptaMA #formal method #simulation #towards #using #validation
Toward Formalizing a Validation Methodology Using Simulation Coverage (AG, SM, PA), pp. 740–745.
CAV-1993-GuptaF #induction #parametricity #representation #using
Parametric Circuit Representation Using Inductive Boolean Functions (AG, ALF), pp. 15–28.
FSE-2016-YogaNG #concurrent #detection #parallel #source code
Parallel data race detection for task parallel programs with locks (AY, SN, AG), pp. 833–845.
CAV-2018-FedyukovichZG #analysis #termination
Syntax-Guided Termination Analysis (GF, YZ, AG), pp. 124–143.
CAV-2018-PickFG #relational #symmetry #verification
Exploiting Synchrony and Symmetry in Relational Verification (LP, GF, AG), pp. 164–182.
CAV-2018-YangVSGM #composition #lazy evaluation #security #self #verification
Lazy Self-composition for Security Verification (WY, YV, PS, AG, SM), pp. 136–156.
CAV-2019-FedyukovichPMG #invariant #quantifier #synthesis
Quantified Invariants via Syntax-Guided Synthesis (GF, SP, KM, AG), pp. 259–277.
POPL-2020-BeckettGMW #abstract interpretation #distributed #network
Abstract interpretation of distributed network control planes (RB, AG, RM, DW), p. 27.
SMT-J-2006-GanaiTG #difference #encoding #integration #lazy evaluation #logic #named
SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic (MKG, MT, AG), pp. 91–114.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.