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: Qadeer:Shaz
Facilitated 4 volumes:
PracticalTrackPrCoPrCo
EdContributed to:
2015
2015
2015
20152014
2014
2013
20132013201220122012
20112010
2010
200920092009
20092009
200820082008200720072007
2006
2006200620052005200420042004200320032002200220022000199919981997
19971996201820182018Wrote 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.