Papers

Recent Publications (after 2005)

Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgstrom, Bayesian Inference Using Data Flow Analysis, in Foundations of Software Engineering (FSE), ACM, August 2013
Arun Chaganty, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani, Combining Relational Learning with SMT Solvers using CEGAR, in Computer Aided Verification (CAV), Lecture Notes in Computer Science, July 2013
Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey, P: Safe Asynchronous Event-Driven Programming, in Programming Languages Design and Implementation (PLDI) 2013, ACM, June 2013
Arun T. Chaganty, Aditya V. Nori, and Sriram K. Rajamani, Efficiently Sampling Probabilistic Programs via Program Analysis, in Artificial Intelligence and Statistics (AISTATS), April 2013
Andrew D. Gordon, Aditya V. Nori, and Sriram K. Rajamani, Probabilistic Inference Using Program Analysis, in Off the Beaten Track (OBT '13), January 2013
Jose Faleiro, Sriram Rajamani, Kaushik Rajan, G Ramalingam, and Kapil Vaswani, Generalized Lattice Agreement, in Principles of Distributed Computing (PODC), ACM, July 2012
Aws Albarghouthi, Rahul Kumar, Aditya V. Nori, and Sriram K. Rajamani, Parallelizing Top-Down Interprocedural Analyses, in Programming Languages Design and Implementation (PLDI), ACM, June 2012
Abhishek Udupa, Ankush Desai, and Sriram Rajamani, Depth bounded explicit-state model checking, in Proceedings of the 18th international SPIN conference on Model checking software, Springer-Verlag, Berlin, Heidelberg, 2011
Aditya Kanade, Rajeev Alur, Sriram Rajamani, and G Ramalingam, Representation Dependence Testing Using Program Inversion, in Foundations of Software Engineering (FSE), Association for Computing Machinery, Inc., November 2010
William R. Harris, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani, Alternation for Termination, in SAS '10: Static Analysis Symposium, Springer Verlag, September 2010
Kaushik Rajan, Sriram Rajamani, and Shashank Yaduvanshi, GUESSTIMATE: A Programming Model for Collaborative Distributed Systems, in Proceedings of Programming Language Design and Implementation (PLDI 2010), Association for Computing Machinery, Inc., June 2010
Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, and Sriram K. Rajamani, Refining Abstract Interpretations, in Information Processing Letters, Elsevier , May 2010
Aditya V. Nori and Sriram K. Rajamani, An Empirical Study of Optimizations in Yogi, in International Conference on Software Engineering (ICSE), Association for Computing Machinery, Inc., May 2010
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, and Aditya V. Thakur, Proofs from Tests, in IEEE Transactions on Software Engineering (special issue on the ISSTA 2008 best papers), IEEE, March 2010
Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and Sai Deep Tetali, Compositional May-Must Program Analysis: Unleashing the Power of Alternation, in Principles of Programming Languages (POPL), Association for Computing Machinery, Inc., January 2010
B. Ashok, Joseph Joy, Hongkang Liang, Sriram Rajamani, Gopal Srinivasa, and Vipindeep Vangala, DebugAdvisor: A Recommender System for Debugging, in Foundations of Software Engineering (ESEC/FSE), Association for Computing Machinery, Inc., 26 August 2009
Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, and Anindya Banerjee, Merlin: Specification Inference for Explicit Information Flow Problems , in ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI), Association for Computing Machinery, Inc., June 2009
Sriram Rajamani, G Ramalingam, Venkatesh Prasad Ranganath, and Kapil Vaswani, Isolator: Dynamically Ensuring Isolation in Concurrent Programs, in Proceedings of the Symposium on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Association for Computing Machinery, Inc., March 2009
Aditya V. Nori, Sriram K. Rajamani, Sai Deep Tetali, and Aditya V. Thakur, The Yogi Project: Software Property Checking via Static Analysis and Testing, in TACAS '09: Tools and Algorithms for the Construction and Analysis of Systems, Springer Verlag, March 2009
Manuel Fahndrich, Sriram K. Rajamani, and Jakob Rehof, Static Deadlock Prevention in Dynamically Configured Communication Networks, in Perspectives On Concurrency, Festchrift for Prof. P. S. Thiagarajan's 60th birthday, K. Lodaya, M. Mukund and R. Ramanujam (eds), Universities Press, December 2008
Shilpa Bugde, Nachi Nagappan, G. Ramalingam, and Sriram Rajamani, Global Software Servicing: Observational Experiences at Microsoft , in International Conference on Global Software Engineering (IGCSE), October 2008
Madhu Gopinathan and Sriram Rajamani, Enforcing Object Protocols by Combining Static and Dynamic Analysis, in ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA), Association for Computing Machinery, Inc., October 2008
Patrice Godefroid, Peli de Halleux, Michael Y. Levin, Aditya V. Nori, Sriram K. Rajamani, Wolfram Schulte, and Nikolai Tillmann, Automated Software Testing Using Program Analysis, in IEEE Software, IEEE Computer Society, October 2008
Avik Chaudhuri, Prasad Naldurg, G. Ramalingam, Sriram Rajamani, and L. Velaga, EON: Modeling and Analyzing Access Control Systems with Logic Programs, in ACM Conference on Computer and Communications Security (CCS), Association for Computing Machinery, Inc., October 2008
Christian Stefansen, Sriram Rajamani, and Parameswaran Seshan, SOFTALLOC: A Workflow Allocation Language with Soft Constraints, in IEEE International Conference on Web Services (ICWS), IEEE Computer Society, September 2008
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, and Robert J. Simmons, Proofs from Tests, in Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), Association for Computing Machinery, Inc., July 2008
Avik Chaudhuri, Prasad Naldurg, and Sriram Rajamani, A Type System for Data-Flow Integrity on Windows Vista, in ACM Workshop on Programming Languages and Analysis for Security (PLAS), Association for Computing Machinery, Inc., June 2008
Sriram Rajamani, G Ramalingam, Venkatesh Prasad Ranganath, and Kapil Vaswani, Controlling Non-determinism for Semantic Guarantees, in Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC2), June 2008
Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, and Sriram K. Rajamani, Automatically Refining Abstract Interpretations, in Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2008
Madhu Gopinathan and Sriram Rajamani, Runtime Verification of Object Invariants with Guarantee, in 8th workshop on Runtime Verification (RV), March 2008
Krishna Mehra, Sriram K. Rajamani, Prasad Sistla, and Sumit K. Jha, Verification of Object-Relational Maps, in Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM), IEEE Computer Society, September 2007
Prakash Chandrasekaran, Christopher L. Conway, Joseph M. Joy, and Sriram K. Rajamani, Programming Asynchronous Layers with CLARITY, in Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Association for Computing Machinery, Inc., September 2007
Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani, Synergy: A New Algorithm for Property Checking, in Proceedings of the 14th Annual Symposium on Foundations of Software Engineering (FSE, ACM SIGSOFT Distinguished Paper) , Association for Computing Machinery, Inc., November 2006
Prasad Naldurg, Stefan Schwoon, Sriram Rajamani, and John Lambert, NETRA: Seeing Through Access Control, in Proceedings of the 4th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE), Association for Computing Machinery, Inc., November 2006
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, and Abdullah Ustuner, Thorough Static Analysis of Device Drivers, in EuroSys 2006, April 2006
Bhargav S. Gulavani and Sriram K. Rajamani, Counterexample driven Refinement for Abstract Interpretation, in Proceedings of 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2006
Sriram Rajamani, Automatic Property Checking for Software: Past, Present and Future, in Proceedings of the 4th International Conference on Software Engineering and Formal Methods (SEFM), IEEE Computer Society, 2006
James R. Larus, Thomas Ball, Manuvir Das, Robert DeLine, Manuel Fähndrich, Jon Pincus, Sriram K. Rajamani, and Ramanathan Venkatapathy, Righting Software, in IEEE Software, vol. 21, no. 3, pp. 92–100, Institute of Electrical and Electronics Engineers, Inc., May 2004

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