Papers
Recent Publications (after 2005)

Publications (before 2005)

 

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

 

2004

·with T. Andrews, S. Qadeer, J. Rehof, and Y. Xie, “Zing: Exploiting Program Structure for Model Checking Concurrent Software”, in Proceedings of the 15th International Conference on Concurrency Theory (CONCUR 04), Lecture Notes in Computer Science 3170, Springer-Verlag, 2004, pp. 1 – 15 (invited paper).

·with T. Andrews, S. Qadeer, J. Rehof, Y. Xie, “Zing: A Model Checker for Concurrent Software”, in Proceedings of the 16th International Conference on Computer Aided Verification (CAV 04), Lecture Notes in Computer Science 3114, Springer-Verlag, 2004, pp. 484 – 487.

·with C. Fournet, C. A. R Hoare and J. Rehof, “Stuck-free Conformance”, in Proceedings of the 16th International Conference on Computer Aided Verification (CAV 04), Lecture Notes in Computer Science 3114, Springer-Verlag, 2004, pp. 242 – 254.

·with T. Ball, B. Cook, V. Levin, “SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft”, ”, Proceedings of the 4th International Conference on Integreated Formal Methods (IFM 2004), Lecture Notes in Computer Science 2999, Springer-Verlag, 2004, pp. 1-20 (invited paper).

·with T. Ball, B. Cook, S. Das, “Refining Approximations in Software Predicate Abstraction”, Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 04), Lecture Notes in Computer Science 2988, Springer-Verlag, 2004, pp. 388-403.

·with S. Qadeer and J. Rehof, “Summarizing Procedures in Multithreaded Programs”, Proceedings of the31st SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 04), ACM, 2004, pp. 245-255.

·with J. Rehof, Models for Contract Conformance, Proceedings of the First International Symposium on Leveraging Applications of Formal Methods, Paphos, Cyprus, October/November 2004.

2003

·with T.Ball and M. Naik, “From Symptom To Cause: Localizing Errors in Counterexample Traces”, Proceedings of the30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 03), ACM, 2003, pp. 97-105.

2002

·with J. Rehof, “Conformance Checking for Models of Asynchronous Message Passing Software”, in Proceedings of the 14th International Conference on Computer Aided Verification (CAV 02), Lecture Notes in Computer Science 2404, Springer-Verlag, 2002.

·with S. Adams, T. Ball, M. Das, S. Lerner, M. Seigle, W. Weimer, “Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis”, in Proceedings of the 9th International Symposium on Static Analysis( SAS 2002), Lecture Notes in Computer Science, Springer-Verlag, 2002.

· with T. Ball, A. Podelski, “Relative Completeness of Abstraction Refinement for Software Model Checking”, in Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002), Lecture Notes in Computer Science 2280, Springer-Verlag, 2002, pp. 158-172.

· with S. Chaki, J. Rehof, “Types as Models: Model Checking Message Passing Programs”, in Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 02), ACM, 2002, pp. 45-57.

· with T. Ball, “The SLAM Project: Debugging System Software via Static Analysis”, in Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 02), ACM, 2002, pp. 1-3 (invited paper)

2001

·with J. Rehof, “A Behavioral Module System for the Pi Calculus”, in Proceedings of the 8th International Symposium on Static Analysis ( SAS 2001), Lecture Notes in Computer Science 2126, Springer-Verlag, 2001, pp. 375-394.

· with T. Ball, “The SLAM Toolkit”, in Proceedings of the 13th International Conference on Computer Aided Verification (CAV 01), Lecture Notes in Computer Science 2102, Springer-Verlag, 2001, pp. 260-264.

· with T. Ball, “Bebop: A Path Sensitive Dataflow Analysis Engine”, in Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering (PASTE 01), ACM, 2001, pp. 97-103.

· with T.Ball, “Automatically Validating Temporal Safety Properties of Interfaces”, in Proceedings of the Eighth International SPIN Workshop (SPIN 01), Lecture Notes in Computer Science 2057, Springer-Verlag, 2001, pp, 103-122.

· with T. Ball, R. Majumdar,T. Millstein, “Automatic Predicate Abstraction of C programs”, in Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 01), ACM, 2001, pp. 203-123.

· with T. Ball, A. Podelski, “Boolean and Cartesian Abstractions for Model Checking C Programs”, in Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 01), Lecture Notes in Computer Science 2031, Springer-Verlag, 2001, pp. 268-283.

· with T.Ball, S. Chaki, “Parameterized Verification of Multithreaded Software Libraries”, in Proceedings of the Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 01), Lecture Notes in Computer Science 2031, Springer-Verlag, 2001, pp. 158-173

2000

· with T. A.Henzinger, S.Qadeer, “Decomposing Refinement Proofs Using Assume-Guarantee Reasoning”, in Proceedings of the International Conference on Computer Aided Design (ICCAD 00), IEEE, pp.242-252. (invited)

· with T. Ball, “Bebop: A Symbolic Model Checker for Boolean Programs”, Proceedings of the 7th International SPIN Workshop (SPIN 00), Lecture Notes in Computer Science 1885, Springer-Verlag, 2000, pp.113-130.

· with T. Ball, “Checking Temporal Properties of Software with Boolean Programs”, Workshop on Advances in Verification (WAVE 00).

· with T.A.Henzinger, “Fair Bisimulation”, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 00), Lecture Notes in Computer Science 1785, Springer-Verlag, 2000, pp. 299-314.

1999

·with T.A.Henzinger, X.Liu, S.Qadeer “Formal Specification and Verification of a Data Flow Processor Array”, Proceedings of the International Conference on Computer Aided Design (ICCAD 99), IEEE, 1999, pp. 494-499.

· with T. A. Henzinger, S. Qadeer “Assume-Guarantee Refinement Between Different Time Scales”, Proceedings of the 10th International Conference on Computer Aided Verification (CAV 99), Lecture Notes in Computer Science 1633, Springer-Verlag, 1999, pp. 208-221.

·with T. A. Henzinger, S. Qadeer “Verifying Sequential Consistency on Shared Memory Multiprocessor Systems”, Proceedings of the 10th International Conference on Computer Aided Verification (CAV 99), Lecture Notes in Computer Science 1633, Springer-Verlag, 1999, pp. 301-315.

1998

· with T.A. Henzinger, S.Qadeer, S.Tasiran, “An Assume-Guarantee Rule for Checking Simulation”, Proceedings of the 2nd International Conference on Formal Methods in Computer Aided Design (FMCAD 98), Lecture Notes in Computer Science 1522, Springer-Verlag, 1998, pp. 440-451

· with T. A.Henzinger, O.Kupferman, “Fair Simulation”, Proceedings of TECHCON 98, Publication #Z98168, Semiconductor Research Corporation, 1998

· with T. A.Henzinger, S.Qadeer, “You Assume, We Guarantee: Methodology and Case Studies”, Proceedings of the 10th International Conference on Computer Aided Verification (CAV 98), Lecture Notes in Computer Science 1427, Springer-Verlag, 1998, pp. 440-451

· with R.Alur, T.A.Henzinger, F.Y.C.Mang, S.Qadeer, S.Tasiran, “MOCHA: Modularity in Model Checking”, Proceedings of the Tenth International Conference on Computer Aided Verification (CAV 98), Lecture Notes in Computer Science 1427, Springer-Verlag, 1998, pp. 521-525

· with R.Alur, T.A.Henzinger, “Symbolic Exploration of Transition Hierarchies”, Proceedings of the Fourth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 98), Lecture Notes in Computer Science 1384, Springer-Verlag 1998, pp. 330-34.

1997

· with T.A.Henzinger, O.Kupferman, “Fair Simulation”, Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR 97), Lecture Notes in Computer Science 1243, 1997, pp. 273-287.

· with R.Alur, R.K.Brayton, T.A.Henzinger, S.Qadeer, “Partial Order Reduction in Symbolic State Space Exploration”, Proceedings of the Ninth International Conference on Computer Aided Verification (CAV 97), Lecture Notes in Computer Science 1254, Springer-Verlag, 1997, pp. 340-351

· with G.Swamy, C.Lennard, R.K.Brayton , “Minimal Logic Resynthesis for Engineering Change”, Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS 97), IEEE Press, 1997, pp. 1596-1599.

· with P.Viswanath, “A Quantitative Analysis of the Processor-Programmable Logic Interface”, Proceedings of the IEEE Symposium on FPGAs for Custom Computing Machines (FCCM 97), IEEE Press, 1997, pp. 226-234.