Sriram K. Rajamani

Microsoft Research India

Papers

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.

 

2008

· with M. Gopinathan, Enforcing Object Protocols by Combining Static and Dynamic Analysis. To appear in OOPSLA '08: ACM SPIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications,  October 2008

· with A. Chaudhuri and P. Naldurg, A Type System for Data-Flow Integrity on Windows Vista, To appear in PLAS '08: ACM Workshop on Programming Languages and Analysis for Security,  June 2008 (also to appear in ACM SIGPLAN notices as one of “two top papers of PLAS 2008”)

· with S. Bugde, N. Nagappan and G. Ramalingam, Global Software Servicing:  Observational Experiences at  Microsoft To appear in IGCSE '08: International Conference on Global Software Engineering,  October 2008

· with N. Beckman, A. Nori and R. Simmons, Proofs from Tests. To appear in ISSTA '08: 14th International Symposium on Testing and Analysis,  July 2008

· with Bhargav S. Gulavani, Supratik Chakraborty, and Aditya V. Nori , Automatically Refining Abstract Interpretations. in TACAS '08: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,  March 2008

· with M. Gopinathan, Runtime Verification of Object Invariants with Guarantee. in  RV '08: 8th workshop on Runtime Verification,  March 2008

 

2007

· With P. Chandrasekaran, C. L. Conway, J. M. Joy,  Programming Asynchronous Layers with CLARITY,   Proceedings of the  6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, September 2007

· With K. K. Mehra, A. P. Sistla and S. K. Jha,  Verification of Object-Relational Maps,   Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods, September 2007

2006

· with B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori , Synergy: A New Algorithm for Property Checking. Proceedings of the 14th Annual Symposium on Foundations of Software Engineering (FSE), ACM Press,  November 2006 (ACM-SIGSOFT Distinguished Paper).

· with P. Naldurg, S. Schwoon, and J. Lambert, NETRA: Seeing Through Access Control,  Proceedings of the 4th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE), November 2006.

· Automatic Property Checking for Software: Past, Present and Future, Proceedings of the 4^th International Conference on Software Engineering and Formal Methods , SEFM 2006 (invited paper).

· with T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, and A. Ustuner, Thorough Static Analysis of Device Drivers, EuroSys 2006, April 2006.

· with B. S. Gulavani, Counterexample driven Refinement for Abstract Interpretation, Proceedings of 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2006.

 

2005

· with V. Levin, R. Palmer and S. Qadeer, Sound Transaction-Based Reduction Without Cycle Detection, in Proceedings of the Twelfth International SPIN Workshop (SPIN 05), Lecture Notes in Computer Science 3639, Springer-Verlag, 2005, pp, 106-122.

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 the31^st 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.