Shaz Qadeer's Publications

Software verification · Protocol verification · Hardware verification · Architecture · Logic synthesis Journal papers

Software verification

T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: Efficiently computing the happens-before relation using locksets. Proceedings of the Workshop on Formal Approaches to Testing and Runtime Verification, 2006. Abstract Pdf
S. Lahiri and S. Qadeer. Verifying properties of well-founded linked lists. To appear in the Proceedings of ACM Symposium on Principles of Programming Languages, 2006. Abstract Pdf
T. Elmas, S. Tasiran, and S. Qadeer. VYRD: Verifying concurrent programs by runtime refinement-violation detection. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005. Abstract Pdf
S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. Proceedings of the 11th International Symposium on Tools and Algorithms for the Construction and Analysis of Systems, 2005. Abstract Postscript
- Extended version appeared as Microsoft Research Technical Report 2004-70, July, 2004. Abstract Postscript
T. Andrews, S. Qadeer, J. Rehof, S.K. Rajamani, and Y. Xie. Zing: Exploiting program structure for model checking concurrent software. Proceedings of the 15th International Conference on Concurrency Theory, 2004. Abstract Postscript
T. Andrews, S. Qadeer, J. Rehof, S.K. Rajamani, and Y. Xie. Zing: A model checker for concurrent software. To appear in the Proceedings of the 16th International Conference on Computer-Aided Verification, 2004. Abstract Postscript
C. Flanagan, S.N. Freund, and S. Qadeer. Exploiting purity for atomicity. To appear in the Proceedings of the International Symposium on Software Testing and Analysis, 2004 (Distinguished Paper Award). Abstract Postscript
S. Qadeer and D. Wu. KISS: Keep it simple and sequential. To appear in the Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2004. Postscript Pdf
S. Tasiran and S. Qadeer. Runtime refinement checking of concurrent data structures. To appear in the Proceedings of the Fourth Workshop on Runtime Verification, 2004. Abstract Postscript
S. Qadeer, S.K. Rajamani and J. Rehof. Summarizing procedures in concurrent programs. Proceedings of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004. Abstract Postscript Pdf
C. Flanagan and S. Qadeer. Transactions for software model checking. Proceedings of the Workshop on Software Model Checking (published as volume 89 of Electronic Notes in Theoretical Computer Science), 2003. Abstract Postscript Pdf

S.N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. Proceedings of the Fifth ECOOP Workshop on Formal Techniques for Java-like Programs, 2003. Abstract Postscript.
T. A. Henzinger, R. Jhala, R. Majumdar and S. Qadeer. Thread-modular abstraction refinement. Proceedings of the International Conference on Computer-Aided Verification, 2003. Abstract Postscript.
C. Flanagan and S. Qadeer. A type and effect system for atomicity. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2003. Abstract Postscript.
C. Flanagan and S. Qadeer. Thread-modular model checking. Proceedings of the SPIN Workshop on Software Verification, 2003. Abstract Postscript.
C. Flanagan and S. Qadeer. Types for atomicity. Proceedings of the Workshop on Types in Language Design and Implementation, 2003. Abstract Postscript.
C. Flanagan, S. Qadeer and S. A. Seshia. A modular checker for multithreaded programs. Proceedings of the International Conference on Computer-Aided Verification, 2002. Abstract Postscript.
C. Flanagan, S. N. Freund and S. Qadeer. Thread-modular verification for shared-memory programs. Proceedings of the European Symposium on Programming, 2002. Abstract Postscript. Full version available as Compaq Systems Research Center Technical Note 2001-003, November 2001.
C. Flanagan and S. Qadeer. Predicate abstraction for software verification. Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002. Abstract Postscript

Protocol verification

J. Bingham, A. Condon, A.J. Hu, S. Qadeer, and Z. Zhang. Automatic verification of sequential consistency for unbounded addresses and data values. Proceedings of 16th International Conference on Computer-Aided Verification, 2004. Abstract Postscript
S. Qadeer. Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Transactions on Parallel and Distributed Systems, vol. 14, no. 8, August 2003. Abstract Postscript. Also available as Research Report 176, Compaq Systems Research Center, December 2001.
K. L. McMillan, S. Qadeer, J. B. Saxe. Induction in compositional model checking. Proceedings of the 12th International Conference on Computer Aided Verification, 2000. Postscript
S. Qadeer. On the verification of memory models of shared-memory multiprocessors. Workshop on Shared-Memory Protocol Verification, 2000 (MPV 2000). Abstract Postscript
T.A. Henzinger, S. Qadeer, S.K. Rajamani. Verifying sequential consistency on shared-memory multiprocessor systems. Proceedings of the 11th International Conference on Computer-Aided Verification, 1999. Postscript.
S. Qadeer, N. Shankar. Verifying a self-stabilizing mutual exclusion algorithm. Proceedings of the IFIP Working Conference on Programming Concepts and Methods, 1998. Postscript.

Hardware verification

S. Qadeer and S. Tasiran. Promising directions in hardware design verification. Proceedings of the 3rd IEEE International Symposium on Quality Electronic Design, 2002. Pdf. Invited Paper.
T.A. Henzinger, S. Qadeer, S. K. Rajamani. Decomposing refinement proofs using assume-guarantee reasoning. Proceedings of the International Conference on Computer-Aided Design, 2000. Postscript. Invited Paper.
S. Qadeer. Algorithms and methodology for scalable model checking. Ph.D. thesis, EECS Department, University of California at Berkeley, 1999. Pdf.
T.A. Henzinger, X. Liu, S. Qadeer, S.K. Rajamani. Formal specification and verification of a dataflow processor array. Proceedings of the International Conference on Computer-Aided Design, 1999. Postscript.
T.A. Henzinger, S. Qadeer, S.K. Rajamani. Assume-guarantee refinement between different time scales. Proceedings of the 11th International Conference on Computer-Aided Verification, 1999. Postscript.
T.A. Henzinger, S. Qadeer, S.K. Rajamani, S. Tasiran. An assume-guarantee rule for checking simulation. Proceedings of the 2nd Conference on Formal Methods in Computer-Aided Design, 1998. Postscript.
T. A. Henzinger, O. Kupferman, S. Qadeer. From pre-historic to post-modern symbolic model checking. Proceedings of the 10th International Conference on Computer-Aided Verification, 1998. Postscript.
T. A. Henzinger, S. Qadeer, S. K. Rajamani You assume, we guarantee: methodology and case studies. Proceedings of the 10th International Conference on Computer-Aided Verification, 1998. Postscript.
R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, S. Tasiran. MOCHA: Modularity in model checking. Proceedings of the 10th International Conference on Computer-Aided Verification, 1998. Postscript.
R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, S. Rajamani. Partial-order reduction in symbolic state-space exploration. Proceedings of the 9th International Conference on Computer-Aided Verification, 1997. Postscript.
J.-Y. Jang, S. Qadeer, C. Pixley, M. Kaufmann. Formal verification of FIRE: A case study. Proceedings of the 34th Design Automation Conference, 1997. Postscript.
R.K. Brayton, G. D. Hachtel, A.L. Sangiovanni-Vincentelli, A. Aziz, F. Somenzi, S.-T. Cheng, S. Edwards, S.P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G.M. Swamy and T. Villa. VIS: a system for verification and synthesis. Proceedings of the 8th International Conference in Computer-Aided Verification, 1996. Postscript.

Architecture

L. A. Barroso, K. Gharachorloo, R. McNamara, A. Nowatzyk, S. Qadeer, B. Sano, S. Smith, R. Stets and B. Verghese. Piranha: a scalable architecture based on single-chip multiprocessing. Proceedings of the 27th Annual International Symposium on Computer Architecture, 2000 (ISCA 2000). Pdf
A. Mehrotra, S. Qadeer, R. K. Ranjan, R. Katz. Benchmarking and analysis of architectures for CAD applications. Proceedings of the International Conference on Computer Design, 1997. Postscript.. Outstanding Paper Award.

Logic synthesis

A. Mehrotra, S. Qadeer, V. Singhal, R. K. Brayton, A. Aziz, A. L. Sangiovanni-Vincentelli. Sequential optimisation without state space exploration. Proceedings of the International Conference on Computer-Aided Design, 1997. Postscript.
S. Qadeer, V. Singhal, C. Pixley, R. K. Brayton. Latch redundancy removal without global reset. Proceedings of the International Conference on Computer Design, 1996. Postscript.

Journal papers

C. Flanagan, S.N. Freund and S. Qadeer. Exploiting purity for atomicity. IEEE Transactions on Software Engineering, 31(4):275-291, April 2005. Pdf
C. Flanagan, S.N. Freund, S. Qadeer and S. A. Seshia. Modular verification of multithreaded programs. Theoretical Computer Science, 338:153-183, June 2005. Download
T. A. Henzinger, O. Kupferman, S. Qadeer. From pre-historic to post-modern symbolic model checking. Formal Methods in System Design, 23:303-327, 2003.
S. Qadeer. Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Transactions on Parallel and Distributed Systems, 14(8):730-741, 2003. Postscript.
V. Singhal, C. Pixley, A. Aziz, S. Qadeer, R.K. Brayton. Sequential optimization in the absence of global reset. IEEE Transactions on Design Automation of Electronic Systems, 8(2):222-251, 2003. Postscript. Pdf.
T.A. Henzinger, S. Qadeer, S.K. Rajamani, S. Tasiran. An assume-guarantee rule for checking simulation. ACM Transactions on Programming Languages and Systems, 24:51-64, 2002. Postscript.
R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, S. Rajamani. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design, 18:97-116, 2001. Postscript.