VIS: A System for Verification and Synthesis. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli; Fabio Somenzi; Adnan Aziz; Szu-Tsung Cheng; Stephen A. Edwards; Sunil P. Khatri; Yuji Kukimoto; Abelardo Pardo; Shaz Qadeer; Rajeev K. Ranjan 001; et al. (CAV, 1996)

VIS. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli; Fabio Somenzi; Adnan Aziz; Szu-Tsung Cheng; Stephen A. Edwards; Sunil P. Khatri; Yuji Kukimoto; Abelardo Pardo; Shaz Qadeer; Rajeev K. Ranjan 001; et al. (FMCAD, 1996)

Latch Redundancy Removal Without Global Reset. - Shaz Qadeer; Robert K. Brayton; Vigyan Singhal (ICCD, 1996)

Formal Verification of FIRE: A Case Study. - Jae-Young Jang; Shaz Qadeer; Matt Kaufmann; Carl Pixley (DAC, 1997)

Sequential optimisation without state space exploration. - Amit Mehrotra; Shaz Qadeer; Vigyan Singhal; Robert K. Brayton; Adnan Aziz; Alberto L. Sangiovanni-Vincentelli (ICCAD, 1997)

Benchmarking and Analysis of Architectures for CAD Applications. - Amit Mehrotra; Shaz Qadeer; Rajeev K. Ranjan 001; Randy H. Katz (ICCD, 1997)

MOCHA: Modularity in Model Checking. - Rajeev Alur; Thomas A. Henzinger; Freddy Y. C. Mang; Shaz Qadeer; Sriram K. Rajamani; Serdar Tasiran (CAV, 1998)

From Pre-historic to Post-modern Symbolic Model Checking. - Thomas A. Henzinger; Orna Kupferman; Shaz Qadeer (CAV, 1998)

You Assume, We Guarantee: Methodology and Case Studies. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (CAV, 1998)

Verifying a self-stabilizing mutual exclusion algorithm. - Shaz Qadeer; Natarajan Shankar (PROCOMET, 1998)

Assume-Guarantee Refinement Between Different Time Scales. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (CAV, 1999)

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (CAV, 1999)

Formal specification and verification of a dataflow processor array. - Thomas A. Henzinger; Xiaojun Liu; Shaz Qadeer; Sriram K. Rajamani (ICCAD, 1999)

Induction in Compositional Model Checking. - Kenneth L. McMillan; Shaz Qadeer; James B. Saxe (CAV, 2000)

Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (ICCAD, 2000)

Piranha: a scalable architecture based on single-chip multiprocessing. - Luiz André Barroso; Kourosh Gharachorloo; Robert McNamara; Andreas Nowatzyk; Shaz Qadeer; Barton Sano; Scott Smith; Robert Stets; Ben Verghese (ISCA, 2000)

Partial-Order Reduction in Symbolic State-Space Exploration. - Rajeev Alur; Robert K. Brayton; Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (Formal Methods Syst. Des., 2001)

A Modular Checker for Multithreaded Programs. - Cormac Flanagan; Shaz Qadeer; Sanjit A. Seshia (CAV, 2002)

Thread-Modular Verification for Shared-Memory Programs. - Cormac Flanagan; Stephen N. Freund; Shaz Qadeer (ESOP, 2002)

Promising Directions in Hardware Design Verification (invited). - Shaz Qadeer; Serdar Tasiran (ISQED, 2002)

Predicate abstraction for software verification. - Cormac Flanagan; Shaz Qadeer (POPL, 2002)

An assume-guarantee rule for checking simulation. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani; Serdar Tasiran (ACM Trans. Program. Lang. Syst., 2002)

Thread-Modular Abstraction Refinement. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Shaz Qadeer (CAV, 2003)

A type and effect system for atomicity. - Cormac Flanagan; Shaz Qadeer (PLDI, 2003)

Thread-Modular Model Checking. - Cormac Flanagan; Shaz Qadeer (SPIN, 2003)

Types for atomicity. - Cormac Flanagan; Shaz Qadeer (TLDI, 2003)

Transactions for Software Model Checking. - Cormac Flanagan; Shaz Qadeer (SoftMC@CAV, 2003)

From Pre-Historic to Post-Modern Symbolic Model Checking. - Thomas A. Henzinger; Orna Kupferman; Shaz Qadeer (Formal Methods Syst. Des., 2003)

Sequential optimization in the absence of global reset. - Vigyan Singhal; Carl Pixley; Adnan Aziz; Shaz Qadeer; Robert K. Brayton (ACM Trans. Design Autom. Electr. Syst., 2003)

Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking. - Shaz Qadeer (IEEE Trans. Parallel Distributed Syst., 2003)

Zing: A Model Checker for Concurrent Software. - Tony Andrews; Shaz Qadeer; Sriram K. Rajamani; Jakob Rehof; Yichen Xie 001 (CAV, 2004)

Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values. - Jesse D. Bingham; Anne Condon; Alan J. Hu; Shaz Qadeer; Zhichuan Zhang (CAV, 2004)

Zing: Exploiting Program Structure for Model Checking Concurrent Software. - Tony Andrews; Shaz Qadeer; Sriram K. Rajamani; Yichen Xie 001 (CONCUR, 2004)

KISS: keep it simple and sequential. - Shaz Qadeer; Dinghao Wu (PLDI, 2004)

Summarizing procedures in concurrent programs. - Shaz Qadeer; Sriram K. Rajamani; Jakob Rehof (POPL, 2004)

Runtime Refinement Checking of Concurrent Data Structures. - Serdar Tasiran; Shaz Qadeer (RV@ETAPS, 2004)

Checking Concise Specifications for Multithreaded Software. - Stephen N. Freund; Shaz Qadeer (J. Object Technol., 2004)

VYRD: verifYing concurrent programs by runtime refinement-violation detection. - Tayfun Elmas; Serdar Tasiran; Shaz Qadeer (PLDI, 2005)

Sound Transaction-Based Reduction Without Cycle Detection. - Vladimir Levin; Robert Palmer; Shaz Qadeer; Sriram K. Rajamani (SPIN, 2005)

Context-Bounded Model Checking of Concurrent Software. - Shaz Qadeer; Jakob Rehof (TACAS, 2005)

Modular verification of multithreaded programs. - Cormac Flanagan; Stephen N. Freund; Shaz Qadeer; Sanjit A. Seshia (Theor. Comput. Sci., 2005)

Exploiting Purity for Atomicity. - Cormac Flanagan; Stephen N. Freund; Shaz Qadeer (IEEE Trans. Software Eng., 2005)

Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (FATES/RV, 2006)

CHESS: Systematic Stress Testing of Concurrent Software. - Madan Musuvathi; Shaz Qadeer (LOPSTR, 2006)

Verifying properties of well-founded linked lists. - Shuvendu K. Lahiri; Shaz Qadeer (POPL, 2006)

Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. - Ahmed Bouajjani; Séverine Fratani; Shaz Qadeer (CAV, 2007)

Goldilocks: a race and transaction-aware java runtime. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (PLDI, 2007)

Iterative context bounding for systematic testing of multithreaded programs. - Madanlal Musuvathi; Shaz Qadeer (PLDI, 2007)

A Reachability Predicate for Analyzing Low-Level Software. - Shaunak Chatterjee; Shuvendu K. Lahiri; Shaz Qadeer; Zvonimir Rakamaric (TACAS, 2007)

Taming Concurrency: A Program Verification Perspective. - Shaz Qadeer (CONCUR, 2008)

Finding and Reproducing Heisenbugs in Concurrent Programs. - Madanlal Musuvathi; Shaz Qadeer; Thomas Ball 001; Gérard Basler; Piramanayagam Arumuga Nainar; Iulian Neamtiu (OSDI, 2008)

Fair stateless model checking. - Madanlal Musuvathi; Shaz Qadeer (PLDI, 2008)

Back to the future: revisiting precise program verification using SMT solvers. - Shuvendu K. Lahiri; Shaz Qadeer (POPL, 2008)

The Case for Context-Bounded Verification of Concurrent Programs. - Shaz Qadeer (SPIN, 2008)

Types for atomicity: Static checking and inference for Java. - Cormac Flanagan; Stephen N. Freund; Marina Lifshin; Shaz Qadeer (ACM Trans. Program. Lang. Syst., 2008)

Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. - Shuvendu K. Lahiri; Shaz Qadeer (CADE, 2009)

Intra-module Inference. - Shuvendu K. Lahiri; Shaz Qadeer; Juan P. Galeotti; Jan W. Voung; Thomas Wies (CAV, 2009)

Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. - Shuvendu K. Lahiri; Shaz Qadeer; Zvonimir Rakamaric (CAV, 2009)

09361 Abstracts Collection - Design and Validation of Concurrent Systems. - Cormac Flanagan; Susanne Graf; Madhusan Parthasarathy; Shaz Qadeer (Design and Validation of Concurrent Systems, 2009)

Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning. - Serdar Tasiran; Ali Sezgin; Shaz Qadeer (Design and Validation of Concurrent Systems, 2009)

Deconstructing concurrency heisenbugs. - Thomas Ball 001; Sebastian Burckhardt; Jonathan de Halleux; Madanlal Musuvathi; Shaz Qadeer (ICSE Companion, 2009)

An annotation assistant for interactive debugging of programs with common synchronization idioms. - Tayfun Elmas; Ali Sezgin; Serdar Tasiran; Shaz Qadeer (PADTAD, 2009)

Unifying type checking and property checking for low-level code. - Jeremy Condit; Brian Hackett; Shuvendu K. Lahiri; Shaz Qadeer (POPL, 2009)

A calculus of atomic actions. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (POPL, 2009)

Algorithmic Verification of Systems Software Using SMT Solvers. - Shaz Qadeer (SAS, 2009)

A low-level memory model and an accompanying reachability predicate. - Shaunak Chatterjee; Shuvendu K. Lahiri; Shaz Qadeer; Zvonimir Rakamaric (Int. J. Softw. Tools Technol. Transf., 2009)

Conflict exceptions: simplifying concurrent language semantics with precise hardware exceptions for data-races. - Brandon Lucia; Luis Ceze; Karin Strauss; Shaz Qadeer; Hans-Juergen Boehm (ISCA, 2010)

Run-Time Verification of Optimistic Concurrency. - Ali Sezgin; Serdar Tasiran; Kivanç Muslu; Shaz Qadeer (RV, 2010)

Preemption Sealing for Efficient Concurrency Testing. - Thomas Ball 001; Sebastian Burckhardt; Katherine E. Coons; Madanlal Musuvathi; Shaz Qadeer (TACAS, 2010)

Simplifying Linearizability Proofs with Reduction and Abstraction. - Tayfun Elmas; Shaz Qadeer; Ali Sezgin; Omer Subasi; Serdar Tasiran (TACAS, 2010)

Abstract Threads. - Shuvendu K. Lahiri; Alexander Malkis; Shaz Qadeer (VMCAI, 2010)

Towards Scalable Modular Checking of User-Defined Properties. - Thomas Ball 001; Brian Hackett; Shuvendu K. Lahiri; Shaz Qadeer; Julien Vanegue (VSTTE, 2010)

Tressa: Claiming the Future. - Ali Sezgin; Serdar Tasiran; Shaz Qadeer (VSTTE, 2010)

Goldilocks: a race-aware Java runtime. - Tayfun Elmas; Shaz Qadeer; Serdar Tasiran (Commun. ACM, 2010)

Poirot - A Concurrency Sleuth. - Shaz Qadeer (ICFEM, 2011)

Call Invariants. - Shuvendu K. Lahiri; Shaz Qadeer (NASA Formal Methods, 2011)

Linear maps. - Shuvendu K. Lahiri; Shaz Qadeer; David Walker 001 (PLPV, 2011)

Delay-bounded scheduling. - Michael Emmi; Shaz Qadeer; Zvonimir Rakamaric (POPL, 2011)

Practical parallel and concurrent programming. - Caitlin Sadowski; Thomas Ball 001; Judith Bishop; Sebastian Burckhardt; Ganesh Gopalakrishnan; Joseph Mayo; Madanlal Musuvathi; Shaz Qadeer; Stephen Toub (SIGCSE, 2011)

How to Shop for Free Online - Security Analysis of Cashier-as-a-Service Based Web Stores. - Rui Wang 010; Shuo Chen 001; XiaoFeng Wang 001; Shaz Qadeer (IEEE Symposium on Security and Privacy, 2011)

Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads - Mohamed Faouzi Atig; Ahmed Bouajjani; Shaz Qadeer (Log. Methods Comput. Sci., 2011)

Predictable and Progressive Testing of Multithreaded Code. - Thomas Ball 001; Sebastian Burckhardt; Peli de Halleux; Madan Musuvathi; Shaz Qadeer (IEEE Softw., 2011)

A Solver for Reachability Modulo Theories. - Akash Lal; Shaz Qadeer; Shuvendu K. Lahiri (CAV, 2012)

RADISH: Always-on sound and complete race detection in software and hardware. - Joseph Devietti; Benjamin P. Wood; Karin Strauss; Luis Ceze; Dan Grossman; Shaz Qadeer (ISCA, 2012)

GPUVerify: a verifier for GPU kernels. - Adam Betts; Nathan Chong; Alastair F. Donaldson; Shaz Qadeer; Paul Thomson (OOPSLA, 2012)

Asynchronous programs with prioritized task-buffers. - Michael Emmi; Akash Lal; Shaz Qadeer (SIGSOFT FSE, 2012)

Preface. - Ganesh Gopalakrishnan; Shaz Qadeer (Formal Methods Syst. Des., 2012)

Runtime verification of concurrency-specific correctness criteria. - Shaz Qadeer; Serdar Tasiran (Int. J. Softw. Tools Technol. Transf., 2012)

Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels. - Peter Collingbourne; Alastair F. Donaldson; Jeroen Ketema; Shaz Qadeer (ESOP, 2013)

Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels. - Nathan Chong; Alastair F. Donaldson; Paul H. J. Kelly; Jeroen Ketema; Shaz Qadeer (OOPSLA, 2013)

P: safe asynchronous event-driven programming. - Ankush Desai; Vivek Gupta; Ethan K. Jackson; Shaz Qadeer; Sriram K. Rajamani; Damien Zufferey (PLDI, 2013)

Reachability Modulo Theories. - Akash Lal; Shaz Qadeer (RP, 2013)

Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization. - Rui Wang 010; Yuchen Zhou; Shuo Chen 001; Shaz Qadeer; David Evans 001; Yuri Gurevich (USENIX Security Symposium, 2013)

Engineering a Static Verification Tool for GPU Kernels. - Ethel Bardsley; Adam Betts; Nathan Chong; Peter Collingbourne; Pantazis Deligiannis; Alastair F. Donaldson; Jeroen Ketema; Daniel Liew; Shaz Qadeer (CAV, 2014)

A program transformation for faster goal-directed search. - Akash Lal; Shaz Qadeer (FMCAD, 2014)

P: a domain-specific language for asynchronous event-driven programming (invited talk abstract). - Shaz Qadeer (WODA+PERTEA@ISSTA, 2014)

Powering the static driver verifier using corral. - Akash Lal; Shaz Qadeer (SIGSOFT FSE, 2014)

Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems. - Ankush Desai; Sanjit A. Seshia; Shaz Qadeer; David Broman; John C. Eidson (CAV (2), 2015)

Automated and Modular Refinement Reasoning for Concurrent Programs. - Chris Hawblitzel; Erez Petrank; Shaz Qadeer; Serdar Tasiran (CAV (2), 2015)

DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. - Akash Lal; Shaz Qadeer (PLDI, 2015)

Systematic testing of asynchronous reactive systems. - Ankush Desai; Shaz Qadeer; Sanjit A. Seshia (ESEC/SIGSOFT FSE, 2015)

Securing Multiparty Online Services Via Certification of Symbolic Transactions. - Eric Yawei Chen; Shuo Chen 001; Shaz Qadeer; Rui Wang 010 (IEEE Symposium on Security and Privacy, 2015)

SMACK+Corral: A Modular Verifier - (Competition Contribution). - Arvind Haran; Montgomery Carter; Michael Emmi; Akash Lal; Shaz Qadeer; Zvonimir Rakamaric (TACAS, 2015)

The Design and Implementation of a Verification Technique for GPU Kernels. - Adam Betts; Nathan Chong; Alastair F. Donaldson; Jeroen Ketema; Shaz Qadeer; Paul Thomson; John Wickerson (ACM Trans. Program. Lang. Syst., 2015)

Uncovering Bugs in Distributed Storage Systems during Testing (Not in Production!). - Pantazis Deligiannis; Matt McCutchen; Paul Thomson; Shuo Chen 001; Alastair F. Donaldson; John Erickson; Cheng Huang; Akash Lal; Rashmi Mudduluru; Shaz Qadeer; Wolfram Schulte (FAST, 2016)

Self-Verifying Execution (Position Paper). - Matt McCutchen; Daniel Song; Shuo Chen 001; Shaz Qadeer (SecDev, 2016)

Lasso detection using partial-state caching. - Rashmi Mudduluru; Pantazis Deligiannis; Ankush Desai; Akash Lal; Shaz Qadeer (FMCAD, 2017)

DRONA: a framework for safe distributed mobile robotics. - Ankush Desai; Indranil Saha; Jianqiao Yang; Shaz Qadeer; Sanjit A. Seshia (ICCPS, 2017)

SVAuth - A Single-Sign-On Integration Solution with Runtime Verification. - Shuo Chen 001; Matt McCutchen; Phuong Cao; Shaz Qadeer; Ravishankar K. Iyer (RV, 2017)

P: Modular and Safe Asynchronous Programming. - Ankush Desai; Shaz Qadeer (RV, 2017)

On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. - Ahmed Bouajjani; Constantin Enea; Kailiang Ji; Shaz Qadeer (CAV (2), 2018)

Layered Concurrent Programs. - Bernhard Kragl; Shaz Qadeer (CAV (1), 2018)

Synchronizing the Asynchronous. - Bernhard Kragl; Shaz Qadeer; Thomas A. Henzinger (CONCUR, 2018)

Verifying Controllers Against Adversarial Examples with Bayesian Optimization. - Shromona Ghosh; Felix Berkenkamp; Gireeja Ranade; Shaz Qadeer; Ashish Kapoor (ICRA, 2018)

Programming Safe Robotics Systems: Challenges and Advances. - Ankush Desai; Shaz Qadeer; Sanjit A. Seshia (ISoLA (2), 2018)

Compositional programming and testing of dynamic distributed systems. - Ankush Desai; Amar Phanishayee; Shaz Qadeer; Sanjit A. Seshia (Proc. ACM Program. Lang., 2018)

Model Checking Concurrent Programs. - Aarti Gupta; Vineet Kahlon; Shaz Qadeer; Tayssir Touili (Handbook of Model Checking, 2018)

Refinement for Structured Concurrent Programs. - Bernhard Kragl; Shaz Qadeer; Thomas A. Henzinger (CAV (1), 2020)

The Move Prover. - Jingyi Emma Zhong; Kevin Cheang; Shaz Qadeer; Wolfgang Grieskamp; Sam Blackshear; Junkil Park; Yoni Zohar; Clark W. Barrett; David L. Dill (CAV (1), 2020)

Inductive sequentialization of asynchronous programs. - Bernhard Kragl; Constantin Enea; Thomas A. Henzinger; Suha Orhun Mutluergil; Shaz Qadeer (PLDI, 2020)

Armada: low-effort verification of high-performance concurrent programs. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (PLDI, 2020)

Exact and Linear-Time Gas-Cost Analysis. - Ankush Das; Shaz Qadeer (SAS, 2020)

Building Reliable Cloud Services Using P# (Experience Report). - Pantazis Deligiannis; Narayanan Ganapathy; Akash Lal; Shaz Qadeer (CoRR, 2020)

Resources: A Safe Language Abstraction for Money. - Sam Blackshear; David L. Dill; Shaz Qadeer; Clark W. Barrett; John C. Mitchell; Oded Padon; Yoni Zohar (CoRR, 2020)

Inductive Sequentialization of Asynchronous Programs (Evaluated Artifact). - Bernhard Kragl; Constantin Enea; Thomas A. Henzinger; Suha Orhun Mutluergil; Shaz Qadeer (Zenodo, 2020)

Building Reliable Cloud Services Using Coyote Actors. - Pantazis Deligiannis; Narayanan Ganapathy; Akash Lal; Shaz Qadeer (SoCC, 2021)

The Civl Verifier. - Bernhard Kragl; Shaz Qadeer (FMCAD, 2021)

Reasoning About Vectors Using an SMT Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. - David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Meng Xu; Jingyi Emma Zhong (TACAS (1), 2022)

The Move Borrow Checker. - Sam Blackshear; John C. Mitchell; Todd Nowacki; Shaz Qadeer (CoRR, 2022)

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Haojun Ma; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (ACM Trans. Program. Lang. Syst., 2022)

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)