Shaz Qadeer

Affiliations:
  • Microsoft Research, Redmond


According to our database1, Shaz Qadeer authored at least 132 papers between 1996 and 2023.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2021, "For contributions to software verification, software testing, and programming languages".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.
J. Autom. Reason., September, 2023

2022
Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility.
ACM Trans. Program. Lang. Syst., 2022

The Move Borrow Checker.
CoRR, 2022

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
The Civl Verifier.
Proceedings of the Formal Methods in Computer Aided Design, 2021

Building Reliable Cloud Services Using Coyote Actors.
Proceedings of the SoCC '21: ACM Symposium on Cloud Computing, 2021

2020
Inductive Sequentialization of Asynchronous Programs (Evaluated Artifact).
Dataset, April, 2020

Resources: A Safe Language Abstraction for Money.
CoRR, 2020

Building Reliable Cloud Services Using P# (Experience Report).
CoRR, 2020

Exact and Linear-Time Gas-Cost Analysis.
Proceedings of the Static Analysis - 27th International Symposium, 2020

Armada: low-effort verification of high-performance concurrent programs.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Inductive sequentialization of asynchronous programs.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

The Move Prover.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Refinement for Structured Concurrent Programs.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2018
Model Checking Concurrent Programs.
Proceedings of the Handbook of Model Checking., 2018

Compositional programming and testing of dynamic distributed systems.
Proc. ACM Program. Lang., 2018

Programming Safe Robotics Systems: Challenges and Advances.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

Verifying Controllers Against Adversarial Examples with Bayesian Optimization.
Proceedings of the 2018 IEEE International Conference on Robotics and Automation, 2018

Synchronizing the Asynchronous.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

Layered Concurrent Programs.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
P: Modular and Safe Asynchronous Programming.
Proceedings of the Runtime Verification - 17th International Conference, 2017

SVAuth - A Single-Sign-On Integration Solution with Runtime Verification.
Proceedings of the Runtime Verification - 17th International Conference, 2017

DRONA: a framework for safe distributed mobile robotics.
Proceedings of the 8th International Conference on Cyber-Physical Systems, 2017

Lasso detection using partial-state caching.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016
Self-Verifying Execution (Position Paper).
Proceedings of the IEEE Cybersecurity Development, 2016

Uncovering Bugs in Distributed Storage Systems during Testing (Not in Production!).
Proceedings of the 14th USENIX Conference on File and Storage Technologies, 2016

2015
The Design and Implementation of a Verification Technique for GPU Kernels.
ACM Trans. Program. Lang. Syst., 2015

SMACK+Corral: A Modular Verifier - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Securing Multiparty Online Services Via Certification of Symbolic Transactions.
Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

Systematic testing of asynchronous reactive systems.
Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015

DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Automated and Modular Refinement Reasoning for Concurrent Programs.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Powering the static driver verifier using corral.
Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16, 2014

P: a domain-specific language for asynchronous event-driven programming (invited talk abstract).
Proceedings of the 2014 Joint International Workshop on Dynamic Analysis (WODA) and Software and System Performance Testing, 2014

A program transformation for faster goal-directed search.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Engineering a Static Verification Tool for GPU Kernels.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization.
Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013, 2013

Reachability Modulo Theories.
Proceedings of the Reachability Problems - 7th International Workshop, 2013

P: safe asynchronous event-driven programming.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels.
Proceedings of the Programming Languages and Systems, 2013

2012
Runtime verification of concurrency-specific correctness criteria.
Int. J. Softw. Tools Technol. Transf., 2012

Preface.
Formal Methods Syst. Des., 2012

Asynchronous programs with prioritized task-buffers.
Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

GPUVerify: a verifier for GPU kernels.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

RADISH: Always-on sound and complete race detection in software and hardware.
Proceedings of the 39th International Symposium on Computer Architecture (ISCA 2012), 2012

A Solver for Reachability Modulo Theories.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Predictable and Progressive Testing of Multithreaded Code.
IEEE Softw., 2011

Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads
Log. Methods Comput. Sci., 2011

How to Shop for Free Online - Security Analysis of Cashier-as-a-Service Based Web Stores.
Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011

Practical parallel and concurrent programming.
Proceedings of the 42nd ACM technical symposium on Computer science education, 2011

Delay-bounded scheduling.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Linear maps.
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, 2011

Call Invariants.
Proceedings of the NASA Formal Methods, 2011

Poirot - A Concurrency Sleuth.
Proceedings of the Formal Methods and Software Engineering, 2011

2010
Goldilocks: a race-aware Java runtime.
Commun. ACM, 2010

Tressa: Claiming the Future.
Proceedings of the Verified Software: Theories, 2010

Towards Scalable Modular Checking of User-Defined Properties.
Proceedings of the Verified Software: Theories, 2010

Abstract Threads.
Proceedings of the Verification, 2010

Simplifying Linearizability Proofs with Reduction and Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Preemption Sealing for Efficient Concurrency Testing.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Run-Time Verification of Optimistic Concurrency.
Proceedings of the Runtime Verification - First International Conference, 2010

Conflict exceptions: simplifying concurrent language semantics with precise hardware exceptions for data-races.
Proceedings of the 37th International Symposium on Computer Architecture (ISCA 2010), 2010

2009
A low-level memory model and an accompanying reachability predicate.
Int. J. Softw. Tools Technol. Transf., 2009

Algorithmic Verification of Systems Software Using SMT Solvers.
Proceedings of the Static Analysis, 16th International Symposium, 2009

A calculus of atomic actions.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Unifying type checking and property checking for low-level code.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

An annotation assistant for interactive debugging of programs with common synchronization idioms.
Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, 2009

Deconstructing concurrency heisenbugs.
Proceedings of the 31st International Conference on Software Engineering, 2009

Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning.
Proceedings of the Design and Validation of Concurrent Systems, 30.08. - 04.09.2009, 2009

09361 Abstracts Collection - Design and Validation of Concurrent Systems.
Proceedings of the Design and Validation of Concurrent Systems, 30.08. - 04.09.2009, 2009

Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Intra-module Inference.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Complexity and Algorithms for Monomial and Clausal Predicate Abstraction.
Proceedings of the Automated Deduction, 2009

2008
Types for atomicity: Static checking and inference for Java.
ACM Trans. Program. Lang. Syst., 2008

The Case for Context-Bounded Verification of Concurrent Programs.
Proceedings of the Model Checking Software, 2008

Back to the future: revisiting precise program verification using SMT solvers.
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Fair stateless model checking.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Finding and Reproducing Heisenbugs in Concurrent Programs.
Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, 2008

Taming Concurrency: A Program Verification Perspective.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

2007
A Reachability Predicate for Analyzing Low-Level Software.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Iterative context bounding for systematic testing of multithreaded programs.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Goldilocks: a race and transaction-aware java runtime.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Verifying properties of well-founded linked lists.
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

CHESS: Systematic Stress Testing of Concurrent Software.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2006

Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets.
Proceedings of the Formal Approaches to Software Testing and Runtime Verification, 2006

2005
Exploiting Purity for Atomicity.
IEEE Trans. Software Eng., 2005

Modular verification of multithreaded programs.
Theor. Comput. Sci., 2005

Context-Bounded Model Checking of Concurrent Software.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Sound Transaction-Based Reduction Without Cycle Detection.
Proceedings of the Model Checking Software, 2005

VYRD: verifYing concurrent programs by runtime refinement-violation detection.
Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, 2005

2004
Checking Concise Specifications for Multithreaded Software.
J. Object Technol., 2004

Runtime Refinement Checking of Concurrent Data Structures.
Proceedings of the Fourth Workshop on Runtime Verification, 2004

Summarizing procedures in concurrent programs.
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

KISS: keep it simple and sequential.
Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

Zing: Exploiting Program Structure for Model Checking Concurrent Software.
Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Zing: A Model Checker for Concurrent Software.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

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

Sequential optimization in the absence of global reset.
ACM Trans. Design Autom. Electr. Syst., 2003

From Pre-Historic to Post-Modern Symbolic Model Checking.
Formal Methods Syst. Des., 2003

Transactions for Software Model Checking.
Proceedings of the 2003 Workshop on Software Model Checking, 2003

Types for atomicity.
Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

Thread-Modular Model Checking.
Proceedings of the Model Checking Software, 2003

A type and effect system for atomicity.
Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

Thread-Modular Abstraction Refinement.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
An assume-guarantee rule for checking simulation.
ACM Trans. Program. Lang. Syst., 2002

Predicate abstraction for software verification.
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Promising Directions in Hardware Design Verification (invited).
Proceedings of the 3rd International Symposium on Quality of Electronic Design, 2002

Thread-Modular Verification for Shared-Memory Programs.
Proceedings of the Programming Languages and Systems, 2002

A Modular Checker for Multithreaded Programs.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Partial-Order Reduction in Symbolic State-Space Exploration.
Formal Methods Syst. Des., 2001

2000
Piranha: a scalable architecture based on single-chip multiprocessing.
Proceedings of the 27th International Symposium on Computer Architecture (ISCA 2000), 2000

Decomposing Refinement Proofs Using Assume-Guarantee Reasoning.
Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design, 2000

Induction in Compositional Model Checking.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Formal specification and verification of a dataflow processor array.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Assume-Guarantee Refinement Between Different Time Scales.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Verifying a self-stabilizing mutual exclusion algorithm.
Proceedings of the Programming Concepts and Methods, 1998

You Assume, We Guarantee: Methodology and Case Studies.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

From <i>Pre</i>-historic to <i>Post</i>-modern Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

MOCHA: Modularity in Model Checking.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997
Benchmarking and Analysis of Architectures for CAD Applications.
Proceedings of the Proceedings 1997 International Conference on Computer Design: VLSI in Computers & Processors, 1997

Sequential optimisation without state space exploration.
Proceedings of the 1997 IEEE/ACM International Conference on Computer-Aided Design, 1997

Formal Verification of FIRE: A Case Study.
Proceedings of the 34st Conference on Design Automation, 1997

1996
Latch Redundancy Removal Without Global Reset.
Proceedings of the 1996 International Conference on Computer Design (ICCD '96), 1996




  Loading...