Shaz Qadeer

Proceedings of the Formal Methods in Computer Aided Design, 2021

Building Reliable Cloud Services Using Coyote Actors.

[BibT_eX]

[DOI]

Proceedings of the SoCC '21: ACM Symposium on Cloud Computing, 2021

2020

Inductive Sequentialization of Asynchronous Programs (Evaluated Artifact).

[BibT_eX]

[DOI]

Constantin Enea

Suha Orhun Mutluergil

Dataset, April, 2020

Resources: A Safe Language Abstraction for Money.

[BibT_eX]

[DOI]

CoRR, 2020

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

[BibT_eX]

[DOI]

CoRR, 2020

Exact and Linear-Time Gas-Cost Analysis.

[BibT_eX]

[DOI]

Ankush Das

Proceedings of the Static Analysis - 27th International Symposium, 2020

Armada: low-effort verification of high-performance concurrent programs.

[BibT_eX]

[DOI]

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Inductive sequentialization of asynchronous programs.

[BibT_eX]

[DOI]

Constantin Enea

Suha Orhun Mutluergil

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

The Move Prover.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Refinement for Structured Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2018

Model Checking Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Compositional programming and testing of dynamic distributed systems.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Programming Safe Robotics Systems: Challenges and Advances.

[BibT_eX]

[DOI]

Ankush Desai

Sanjit A. Seshia

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

Verifying Controllers Against Adversarial Examples with Bayesian Optimization.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE International Conference on Robotics and Automation, 2018

Synchronizing the Asynchronous.

[BibT_eX]

[DOI]

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

Layered Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

P: Modular and Safe Asynchronous Programming.

[BibT_eX]

[DOI]

Ankush Desai

Proceedings of the Runtime Verification - 17th International Conference, 2017

SVAuth - A Single-Sign-On Integration Solution with Runtime Verification.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 17th International Conference, 2017

DRONA: a framework for safe distributed mobile robotics.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Cyber-Physical Systems, 2017

Lasso detection using partial-state caching.

[BibT_eX]

[DOI]

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

Self-Verifying Execution (Position Paper).

[BibT_eX]

[DOI]

Proceedings of the IEEE Cybersecurity Development, 2016

Uncovering Bugs in Distributed Storage Systems during Testing (Not in Production!).

[BibT_eX]

[DOI]

Proceedings of the 14th USENIX Conference on File and Storage Technologies, 2016

2015

The Design and Implementation of a Verification Technique for GPU Kernels.

[BibT_eX]

[DOI]

Adam Betts

Nathan Chong

ACM Trans. Program. Lang. Syst., 2015

SMACK+Corral: A Modular Verifier - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Securing Multiparty Online Services Via Certification of Symbolic Transactions.

[BibT_eX]

[DOI]

Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

Systematic testing of asynchronous reactive systems.

[BibT_eX]

[DOI]

Ankush Desai

Sanjit A. Seshia

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.

[BibT_eX]

[DOI]

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Automated and Modular Refinement Reasoning for Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Powering the static driver verifier using corral.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Engineering a Static Verification Tool for GPU Kernels.

[BibT_eX]

[DOI]

Jeroen Ketema

Daniel Liew

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization.

[BibT_eX]

[DOI]

Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013, 2013

Reachability Modulo Theories.

[BibT_eX]

[DOI]

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

P: safe asynchronous event-driven programming.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Nathan Chong

Paul H. J. Kelly

Jeroen Ketema

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.

[BibT_eX]

[DOI]

Peter Collingbourne

Jeroen Ketema

Proceedings of the Programming Languages and Systems, 2013

2012

Runtime verification of concurrency-specific correctness criteria.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2012

Preface.

[BibT_eX]

[DOI]

Ganesh Gopalakrishnan

Formal Methods Syst. Des., 2012

Asynchronous programs with prioritized task-buffers.

[BibT_eX]

[DOI]

Michael Emmi

Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

GPUVerify: a verifier for GPU kernels.

[BibT_eX]

[DOI]

Adam Betts

Nathan Chong

Paul Thomson

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.

[BibT_eX]

[DOI]

Proceedings of the 39th International Symposium on Computer Architecture (ISCA 2012), 2012

A Solver for Reachability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Predictable and Progressive Testing of Multithreaded Code.

[BibT_eX]

[DOI]

IEEE Softw., 2011

Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads

[BibT_eX]

[DOI]

Mohamed Faouzi Atig

Ahmed Bouajjani

Log. Methods Comput. Sci., 2011

How to Shop for Free Online - Security Analysis of Cashier-as-a-Service Based Web Stores.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011

Practical parallel and concurrent programming.

[BibT_eX]

[DOI]

Ganesh Gopalakrishnan

Proceedings of the 42nd ACM technical symposium on Computer science education, 2011

Delay-bounded scheduling.

[BibT_eX]

[DOI]

Michael Emmi

Zvonimir Rakamaric

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

Linear maps.

[BibT_eX]

[DOI]

David Walker

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

Call Invariants.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2011

Poirot - A Concurrency Sleuth.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2011

2010

Goldilocks: a race-aware Java runtime.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Tressa: Claiming the Future.

[BibT_eX]

[DOI]

Ali Sezgin

Proceedings of the Verified Software: Theories, 2010

Towards Scalable Modular Checking of User-Defined Properties.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2010

Abstract Threads.

[BibT_eX]

[DOI]

Alexander Malkis

Proceedings of the Verification, 2010

Simplifying Linearizability Proofs with Reduction and Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Preemption Sealing for Efficient Concurrency Testing.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Run-Time Verification of Optimistic Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - First International Conference, 2010

Conflict exceptions: simplifying concurrent language semantics with precise hardware exceptions for data-races.

[BibT_eX]

[DOI]

Proceedings of the 37th International Symposium on Computer Architecture (ISCA 2010), 2010

2009

A low-level memory model and an accompanying reachability predicate.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2009

Algorithmic Verification of Systems Software Using SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 16th International Symposium, 2009

A calculus of atomic actions.

[BibT_eX]

[DOI]

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Unifying type checking and property checking for low-level code.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, 2009

Deconstructing concurrency heisenbugs.

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Software Engineering, 2009

Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning.

[BibT_eX]

[DOI]

Ali Sezgin

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

09361 Abstracts Collection - Design and Validation of Concurrent Systems.

[BibT_eX]

[DOI]

Susanne Graf

Madhusan Parthasarathy

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.

[BibT_eX]

[DOI]

Zvonimir Rakamaric

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Intra-module Inference.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Complexity and Algorithms for Monomial and Clausal Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Types for atomicity: Static checking and inference for Java.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2008

The Case for Context-Bounded Verification of Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2008

Back to the future: revisiting precise program verification using SMT solvers.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Fair stateless model checking.

[BibT_eX]

[DOI]

Madanlal Musuvathi

Piramanayagam Arumuga Nainar

Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Finding and Reproducing Heisenbugs in Concurrent Programs.

[BibT_eX]

[DOI]

Iulian Neamtiu

Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, 2008

Taming Concurrency: A Program Verification Perspective.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

2007

A Reachability Predicate for Analyzing Low-Level Software.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Iterative context bounding for systematic testing of multithreaded programs.

[BibT_eX]

[DOI]

Madanlal Musuvathi

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Goldilocks: a race and transaction-aware java runtime.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures.

[BibT_eX]

[DOI]

Ahmed Bouajjani

Séverine Fratani

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Verifying properties of well-founded linked lists.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

CHESS: Systematic Stress Testing of Concurrent Software.

[BibT_eX]

[DOI]

Madan Musuvathi

Proceedings of the Logic-Based Program Synthesis and Transformation, 2006

Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets.

[BibT_eX]

[DOI]

Proceedings of the Formal Approaches to Software Testing and Runtime Verification, 2006

2005

Exploiting Purity for Atomicity.

[BibT_eX]

[DOI]

Stephen N. Freund

IEEE Trans. Software Eng., 2005

Modular verification of multithreaded programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Context-Bounded Model Checking of Concurrent Software.

[BibT_eX]

[DOI]

Jakob Rehof

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Sound Transaction-Based Reduction Without Cycle Detection.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2005

VYRD: verifYing concurrent programs by runtime refinement-violation detection.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, 2005

2004

Checking Concise Specifications for Multithreaded Software.

[BibT_eX]

[DOI]

Stephen N. Freund

J. Object Technol., 2004

Runtime Refinement Checking of Concurrent Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Fourth Workshop on Runtime Verification, 2004

Summarizing procedures in concurrent programs.

[BibT_eX]

[DOI]

Jakob Rehof

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

KISS: keep it simple and sequential.

[BibT_eX]

[DOI]

Dinghao Wu

Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

Zing: Exploiting Program Structure for Model Checking Concurrent Software.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Zing: A Model Checker for Concurrent Software.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking.

[BibT_eX]

[DOI]

IEEE Trans. Parallel Distributed Syst., 2003

Sequential optimization in the absence of global reset.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2003

From Pre-Historic to Post-Modern Symbolic Model Checking.

[BibT_eX]

[DOI]

Orna Kupferman

Formal Methods Syst. Des., 2003

Transactions for Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 2003 Workshop on Software Model Checking, 2003

Types for atomicity.

[BibT_eX]

[DOI]

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

Thread-Modular Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2003

A type and effect system for atomicity.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

Thread-Modular Abstraction Refinement.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

An assume-guarantee rule for checking simulation.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2002

Predicate abstraction for software verification.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

Proceedings of the 3rd International Symposium on Quality of Electronic Design, 2002

Thread-Modular Verification for Shared-Memory Programs.

[BibT_eX]

[DOI]

Stephen N. Freund

Proceedings of the Programming Languages and Systems, 2002

A Modular Checker for Multithreaded Programs.

[BibT_eX]

[DOI]

Sanjit A. Seshia

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Partial-Order Reduction in Symbolic State-Space Exploration.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

2000

Piranha: a scalable architecture based on single-chip multiprocessing.

[BibT_eX]

[DOI]

Proceedings of the 27th International Symposium on Computer Architecture (ISCA 2000), 2000

Decomposing Refinement Proofs Using Assume-Guarantee Reasoning.

[BibT_eX]

[DOI]

Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design, 2000

Induction in Compositional Model Checking.

[BibT_eX]

[DOI]

Kenneth L. McMillan

James B. Saxe

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Formal specification and verification of a dataflow processor array.

[BibT_eX]

[DOI]

Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Assume-Guarantee Refinement Between Different Time Scales.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

Verifying a self-stabilizing mutual exclusion algorithm.

[BibT_eX]

Natarajan Shankar

Proceedings of the Programming Concepts and Methods, 1998

You Assume, We Guarantee: Methodology and Case Studies.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

From <i>Pre</i>-historic to <i>Post</i>-modern Symbolic Model Checking.

[BibT_eX]

[DOI]

Orna Kupferman

Alberto L. Sangiovanni-Vincentelli

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

MOCHA: Modularity in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

Benchmarking and Analysis of Architectures for CAD Applications.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1997 International Conference on Computer Design: VLSI in Computers & Processors, 1997

Sequential optimisation without state space exploration.

[BibT_eX]

[DOI]

Proceedings of the 1997 IEEE/ACM International Conference on Computer-Aided Design, 1997

Formal Verification of FIRE: A Case Study.

[BibT_eX]

[DOI]

Proceedings of the 34st Conference on Design Automation, 1997

1996

Latch Redundancy Removal Without Global Reset.

[BibT_eX]

[DOI]