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 × Austria
1 × China
1 × Cyprus
1 × Denmark
1 × Germany
1 × Israel
1 × Portugal
1 × Spain
2 × Canada
2 × France
25 × USA
3 × United Kingdom
5 × Italy
Collaborated with:
S.K.Lahiri S.K.Rajamani S.Tasiran T.A.Henzinger A.Lal C.Flanagan T.Elmas M.Musuvathi S.A.Seshia Z.Rakamaric J.Rehof A.Desai A.Bouajjani M.Emmi A.F.Donaldson J.Ketema N.Chong M.Musuvathi D.Wu B.Kragl T.Ball R.Alur P.Collingbourne A.Malkis M.F.Atig S.Fratani S.N.Freund K.L.McMillan J.B.Saxe O.Kupferman A.Betts R.K.Brayton C.Hawblitzel E.Petrank J.Condit B.Hackett S.Chatterjee R.Jhala R.Majumdar J.Jang M.Kaufmann C.Pixley C.Enea K.Ji A.Phanishayee D.Broman J.C.Eidson P.H.J.Kelly P.Thomson S.Burckhardt K.E.Coons A.Sezgin O.Subasi J.P.Galeotti J.W.Voung T.Wies T.Andrews Y.Xie J.D.Bingham A.Condon A.J.Hu Z.Zhang A.Haran M.Carter V.Gupta E.K.Jackson D.Zufferey G.Basler P.A.Nainar I.Neamtiu F.Y.C.Mang E.Bardsley P.Deligiannis D.Liew G.D.Hachtel A.L.Sangiovanni-Vincentelli F.Somenzi A.Aziz S.Cheng S.A.Edwards S.P.Khatri Y.Kukimoto A.Pardo R.K.Ranjan S.Sarwary T.R.Shiple G.Swamy T.Villa
Talks about:
program (16) concurr (11) verif (9) verifi (8) system (8) abstract (7) check (7) softwar (6) modular (6) model (6)

♂ Person: Shaz Qadeer

DBLP DBLP: Qadeer:Shaz

Facilitated 4 volumes:

MoDELS 2014PracticalTrackPrCo
MoDELS 2014PrCo
CAV 2011Ed

Contributed to:

CAV 20152015
ESEC/FSE 20152015
PLDI 20152015
TACAS 20152015
CAV 20142014
FSE 20142014
ESOP 20132013
OOPSLA 20132013
PLDI 20132013
CAV 20122012
FSE 20122012
OOPSLA 20122012
POPL 20112011
TACAS 20102010
VMCAI 20102010
CADE 20092009
CAV 20092009
POPL 20092009
SAS 20092009
TACAS 20092009
OSDI 20082008
PLDI 20082008
POPL 20082008
CAV 20072007
PLDI 20072007
TACAS 20072007
FATES/RV 20062006
LOPSTR 20062006
POPL 20062006
PLDI 20052005
TACAS 20052005
CAV 20042004
PLDI 20042004
POPL 20042004
CAV 20032003
PLDI 20032003
CAV 20022002
ESOP 20022002
POPL 20022002
CAV 20002000
CAV 19991999
CAV 19981998
CAV 19971997
DAC 19971997
CAV 19961996
CAV (1) 20182018
CAV (2) 20182018
OOPSLA 20182018

Wrote 57 papers:

CAV-2015-DesaiSQBE #abstraction #approximate #distributed
Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems (AD, SAS, SQ, DB, JCE), pp. 429–448.
CAV-2015-HawblitzelPQT #automation #composition #concurrent #reasoning #refinement #source code
Automated and Modular Refinement Reasoning for Concurrent Programs (CH, EP, SQ, ST), pp. 449–465.
ESEC-FSE-2015-DesaiQS #testing
Systematic testing of asynchronous reactive systems (AD, SQ, SAS), pp. 73–83.
PLDI-2015-LalQ #graph #source code
DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs (AL, SQ), pp. 280–290.
TACAS-2015-HaranCELQR #composition #contest #verification
SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.
CAV-2014-BardsleyBCCDDKLQ #gpu #kernel #verification
Engineering a Static Verification Tool for GPU Kernels (EB, AB, NC, PC, PD, AFD, JK, DL, SQ), pp. 226–242.
FSE-2014-LalQ #using #verification
Powering the static driver verifier using corral (AL, SQ), pp. 202–212.
ESOP-2013-CollingbourneDKQ #analysis #gpu #kernel #semantics #verification
Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels (PC, AFD, JK, SQ), pp. 270–289.
OOPSLA-2013-ChongDKKQ #abstraction #analysis #gpu #invariant #kernel
Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels (NC, AFD, PHJK, JK, SQ), pp. 605–622.
PLDI-2013-DesaiGJQRZ #named #programming
P: safe asynchronous event-driven programming (AD, VG, EKJ, SQ, SKR, DZ), pp. 321–332.
CAV-2012-LalQL #modulo theories #reachability
A Solver for Reachability Modulo Theories (AL, SQ, SKL), pp. 427–443.
FSE-2012-EmmiLQ #source code
Asynchronous programs with prioritized task-buffers (ME, AL, SQ), p. 48.
OOPSLA-2012-BettsCDQT #gpu #kernel #named #verification
GPUVerify: a verifier for GPU kernels (AB, NC, AFD, SQ, PT), pp. 113–132.
POPL-2011-EmmiQR #bound #scheduling
Delay-bounded scheduling (ME, SQ, ZR), pp. 411–422.
TACAS-2010-BallBCMQ #concurrent #performance #testing
Preemption Sealing for Efficient Concurrency Testing (TB, SB, KEC, MM, SQ), pp. 420–434.
TACAS-2010-ElmasQSST #abstraction #proving #reduction
Simplifying Linearizability Proofs with Reduction and Abstraction (TE, SQ, AS, OS, ST), pp. 296–311.
VMCAI-2010-LahiriMQ #thread
Abstract Threads (SKL, AM, SQ), pp. 231–246.
CADE-2009-LahiriQ #abstraction #algorithm #complexity
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction (SKL, SQ), pp. 214–229.
CAV-2009-LahiriQGVW
Intra-module Inference (SKL, SQ, JPG, JWV, TW), pp. 493–508.
CAV-2009-LahiriQR #concurrent #detection #fault #precise #smt #using
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers (SKL, SQ, ZR), pp. 509–524.
POPL-2009-ConditHLQ #low level #type checking
Unifying type checking and property checking for low-level code (JC, BH, SKL, SQ), pp. 302–314.
POPL-2009-ElmasQT #calculus
A calculus of atomic actions (TE, SQ, ST), pp. 2–15.
SAS-2009-Qadeer #algorithm #smt #using #verification
Algorithmic Verification of Systems Software Using SMT Solvers (SQ), p. 2.
TACAS-2009-AtigBQ #analysis #bound #concurrent #source code #thread
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads (MFA, AB, SQ), pp. 107–123.
OSDI-2008-MusuvathiQBBNN #concurrent #source code
Finding and Reproducing Heisenbugs in Concurrent Programs (MM, SQ, TB, GB, PAN, IN), pp. 267–280.
PLDI-2008-MusuvathiQ #model checking
Fair stateless model checking (MM, SQ), pp. 362–371.
POPL-2008-LahiriQ #precise #smt #using #verification
Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.
CAV-2007-BouajjaniFQ #analysis #bound #parallel #source code #thread
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures (AB, SF, SQ), pp. 207–220.
PLDI-2007-ElmasQT #java #named #runtime #transaction
Goldilocks: a race and transaction-aware java runtime (TE, SQ, ST), pp. 245–255.
PLDI-2007-MusuvathiQ #bound #parallel #source code #testing #thread
Iterative context bounding for systematic testing of multithreaded programs (MM, SQ), pp. 446–455.
TACAS-2007-ChatterjeeLQR #bytecode #low level #reachability
A Reachability Predicate for Analyzing Low-Level Software (SC, SKL, SQ, ZR), pp. 19–33.
FATES-RV-2006-ElmasQT #named #using
Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets (TE, SQ, ST), pp. 193–208.
LOPSTR-2006-MusuvathiQ #concurrent #named #testing
CHESS: Systematic Stress Testing of Concurrent Software (MM, SQ), pp. 15–16.
POPL-2006-LahiriQ #verification
Verifying properties of well-founded linked lists (SKL, SQ), pp. 115–126.
PLDI-2005-ElmasTQ #concurrent #detection #named #runtime #source code #verification
VYRD: verifYing concurrent programs by runtime refinement-violation detection (TE, ST, SQ), pp. 27–37.
TACAS-2005-QadeerR #bound #concurrent #model checking
Context-Bounded Model Checking of Concurrent Software (SQ, JR), pp. 93–107.
CAV-2004-AndrewsQRRX #concurrent #model checking #named
Zing: A Model Checker for Concurrent Software (TA, SQ, SKR, JR, YX), pp. 484–487.
CAV-2004-BinghamCHQZ #automation #bound #consistency #verification
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values (JDB, AC, AJH, SQ, ZZ), pp. 427–439.
PLDI-2004-QadeerW #named
KISS: keep it simple and sequential (SQ, DW), pp. 14–24.
POPL-2004-QadeerRR #concurrent #source code
Summarizing procedures in concurrent programs (SQ, SKR, JR), pp. 245–255.
CAV-2003-HenzingerJMQ #abstraction #refinement #thread
Thread-Modular Abstraction Refinement (TAH, RJ, RM, SQ), pp. 262–274.
PLDI-2003-FlanaganQ
A type and effect system for atomicity (CF, SQ), pp. 338–349.
CAV-2002-FlanaganQS #composition #parallel #source code #thread
A Modular Checker for Multithreaded Programs (CF, SQ, SAS), pp. 180–194.
ESOP-2002-FlanaganFQ #source code #thread #verification
Thread-Modular Verification for Shared-Memory Programs (CF, SNF, SQ), pp. 262–277.
POPL-2002-FlanaganQ #abstraction #verification
Predicate abstraction for software verification (CF, SQ), pp. 191–202.
CAV-2000-McMillanQS #composition #induction #model checking
Induction in Compositional Model Checking (KLM, SQ, JBS), pp. 312–327.
CAV-1999-HenzingerQR #refinement
Assume-Guarantee Refinement Between Different Time Scales (TAH, SQ, SKR), pp. 208–221.
CAV-1999-HenzingerQR99a #consistency #multi #verification
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems (TAH, SQ, SKR), pp. 301–315.
CAV-1998-AlurHMQRT #composition #model checking #named
MOCHA: Modularity in Model Checking (RA, TAH, FYCM, SQ, SKR, ST), pp. 521–525.
CAV-1998-HenzingerKQ #model checking
From Pre-historic to Post-modern Symbolic Model Checking (TAH, OK, SQ), pp. 195–206.
CAV-1998-HenzingerQR #case study
You Assume, We Guarantee: Methodology and Case Studies (TAH, SQ, SKR), pp. 440–451.
CAV-1997-AlurBHQR #partial order #reduction
Partial-Order Reduction in Symbolic State Space Exploration (RA, RKB, TAH, SQ, SKR), pp. 340–351.
DAC-1997-JangQKP #case study #verification
Formal Verification of FIRE: A Case Study (JYJ, SQ, MK, CP), pp. 173–177.
CAV-1996-BraytonHSSACEKKPQRSSSV #named #synthesis #verification
VIS: A System for Verification and Synthesis (RKB, GDH, ALSV, FS, AA, STC, SAE, SPK, YK, AP, SQ, RKR, SS, TRS, GS, TV), pp. 428–432.
CAV-2018-KraglQ #concurrent #source code
Layered Concurrent Programs (BK, SQ), pp. 79–102.
CAV-2018-BouajjaniEJQ #bound #message passing #on the #source code #verification
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony (AB, CE, KJ, SQ), pp. 372–391.
OOPSLA-2018-DesaiPQS #composition #distributed #programming #testing
Compositional programming and testing of dynamic distributed systems (AD, AP, SQ, SAS), p. 30.

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.