Sarfraz Khurshid ACES 5.120 The University of Texas at Austin Electrical and Computer Engineering 1 University Station C5000 Austin, TX 78712-0240 USA Tel: +1 (512) 471 8244 Fax: +1 (512) 471 5120 khurshid@ece.utexas.edu

I am an Associate Professor in the Department of Electrical and Computer Engineering at the University of Texas at Austin in the Center for Advanced Research in Software Engineering (ARiSE). I was formerly a graduate student at the MIT Laboratory for Computer Science, where I co-led the MulSaw project. I defended my PhD thesis in December 2003. A PDF version of my dissertation is available here *.pdf.

My research interests include automated software engineering, in particular: software testing; static and dynamic checking of code conformance; repair of structurally complex data; model checking; formal specification languages; parallel and incremental algorithms for software analysis.

I am a recipient of the ACM SIGSOFT Impact Paper Award (2012), two ACM SIGSOFT Distinguished Paper Awards (ISSTA 2002 and ICSE 2010), a Best Research Paper Award (ASWEC 2009), and an NSF CAREER Award (2009).

My research is funded in part by the National Science Foundation (CAREER award CCF-0845628, and awards CNS-0958231, IIS-0438967, and CCF-0702680), the Air Force Office of Scientific Research, and the Naval Undersea Warfare Center.

Students (Current)

• Doctoral
  • Diego Funes
  • Divya Gopinath (M.S. (Thesis) 2010, UT ECE)
  • Sam Harwell
  • Chang Hwan Peter Kim (UT CS; co-supervised with Prof. Don Batory)
  • Muhammad Zubair Malik (M.S. (Thesis) 2007, UT ECE)
  • Shounak Roychowdhury
  • Guowei Yang
  • Razieh Nokhbeh Zaeem (M.S. (Thesis) 2010, UT ECE)
  • Lingming Zhang
• Undergraduate
  Mehmet Erol Yesin

Students (Former)

• Doctoral
  • Engin Uzuncaova (Ph.D. 2008, UT ECE, Dissertation title: "Efficient Specification-based Testing Using Incremental Techniques", First job after Ph.D.: Microsoft)
  • Bassem Elkarablieh (Ph.D. 2009, UT ECE, Dissertation title: "Assertion-based Repair of Complex Data Structures", First job after Ph.D.: Google)
  • Danhua Shao (Co-supervised with: Prof. Dewayne E. Perry; Ph.D. 2010, UT ECE, Dissertation title: "Application of Local Semantic Analysis in Fault Prediciton and Detection", First job after Ph.D.: Yahoo; also, M.S. (Thesis) 2009 at UT ECE)
  • Shadi Abdul Khalek (Ph.D. 2011, UT ECE, Dissertation title: "Systematic Testing Using Test Summaries: Effective and Efficient Testing of Relational Applications", First job after Ph.D.: Google; also, M.S. (Thesis) 2009 at UT ECE)
  • Junaid Haroon Siddiqui (Ph.D. 2012, UT ECE, Dissertation title: "Improving Systematic Constraint-driven Analysis using Incremental and Parallel Techniques", First job after Ph.D.: Assistant Professor, LUMS CS)
• Masters
  • Ivan Garcia (M.S. (Thesis) 2005, UT ECE)
  • Yuk Lai Suen (M.S. (Thesis) 2005, UT ECE)
  • Daryl Shannon (M.S. (Report) 2005, UT ECE)
  • Khalid Ghori (M.S. (Thesis) 2006, UT ECE)
  • Daniel Garcia (M.S. (Thesis) 2006, UT ECE)
  • Alison Lee (M.S. (Thesis) 2007, UT ECE)
  • Muhammad Younas (M.S. (Thesis) 2007, UT ECE)
  • Lavanya Chockalingam (M.S. (Thesis) 2007, UT ECE)
  • Amresh Kulkarni (M.S. (Thesis) 2007, UT ECE)
  • Daiqian Zhan (M.S. (Thesis) 2007, UT ECE)
  • Vidya Narayanan (M.S. (Thesis) 2009, UT ECE)
  • Sowmiya Chocka Narayanan (M.S. (Thesis) 2010, UT ECE)
• Undergraduate
  • Michael Lin (Undergraduate Researcher, 2005)
  • Sonik Shah (Undergraduate Researcher, 2007)
  • Christopher Tsai (Undergraduate Researcher, 2007)
  • Niyantha Shekar (Undergraduate Researcher, 2009)

Teaching

• Graduate Course
  • EE382C Verification and Validation of Software, Spring 2004, Fall 2004, Spring 2005 (Option III), Fall 2005, Spring 2006 (also Option III), Fall 2006, Spring 2007 (Option III), Spring 2008 (Option III), Fall 2008. (Accessible via UT's blackboard system.)
• Undergraduate Courses
  • EE379K Software Testing, Fall 2006, Spring 2009. (Accessible via UT's blackboard system.)
  • EE360C Algorithms, Fall 2008. (Accessible via UT's blackboard system.)
  • EE322C Data Structures, Spring 2005, Spring 2006, Spring 2007, Fall 2007, Spring 2008. (Accessible via UT's blackboard system.)

Community

• 2012: ABZ: Alloy track PC Chair, ASE ERP, FM PC, FSE PC, ICST PC, JPF PC, Regression PC, RV PC
• 2011: RV PC Co-chair, ASE PC, ATVA PC, CSTVA PC, FM PC, ICST PC, ISSTA PC, JPF PC, NFM PC
• 2010: ABZ: Alloy track PC Chair, SSEAT Co-organizer, RV PC, CSTVA PC
• 2009: OOPSLA PC, ASE ERP, ICST PC, SPIN PC, ICSE Research Demo Track PC
• 2008: ISSTA PC, ASE ERP, SPIN PC, STEP PC, ICST student track PC, FACS PC
• 2007: ASE ERP, IWLU (ASE Workshop) PC
• 2006: ASE PC, FSE Poster Track PC, SOQUA (FSE Workshop) PC, Alloy (FSE Workshop) PC
• 2005: SPIN PC, ICSE Research Demo Track PC
• National Science Foundation Panels

Conference Proceedings (co-edited)

• J. Derrick, J. A. Fitzgerald, S. Gnesi, S. Khurshid, M. Leuschel, S. Reeves, and E. Riccobene, editors. Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012) Proceedings, Pisa, Italy, June 18-21, 2012, Lecture Notes in Computer Science (LNCS) Volume 7316, Springer 2012
• S. Khurshid and K. Sen, editors. Second International Conference on Runtime Verification (RV 2011) Proceedings, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers, Lecture Notes in Computer Science (LNCS) Volume 7186, Springer 2012
• M. Frappier, U. Glasser, S. Khurshid, R. Laleau, and S. Reeves, editors. Second International Conference on Abstract State Machines, Alloy, B and Z (ABZ 2010) Proceedings, Orford, QC, Canada, February 22-25, 2010, Lecture Notes in Computer Science (LNCS) Volume 5977, Springer 2010

Research

• Software Testing, Symbolic Execution, and Model Checking
  • C. Boyapati, S. Khurshid, and D. Marinov. Systematic Software Testing: The Korat Approach -- ACM SIGSOFT Impact Paper Award 2012. ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE), 1 page, Research Triangle Park, NC, November 2012. Keynote (To appear)
  • R. N. Zaeem and S. Khurshid. Test Input Generation Using Dynamic Programming. ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE), 11 pages, Research Triangle Park, NC, November 2012 (To appear)
  • D. Funes, J. H. Siddiqui, and S. Khurshid. Ranged Model Checking. Java Pathfinder Workshop (JPF) 2012, 5 pages, Research Triangle Park, NC, November 2012 (To appear)
  • C. H. P. Kim, S. Khurshid, and D. Batory. Shared Execution for Efficiently Testing Product Lines. 23rd IEEE International Symposium on Software Reliability Engineering (ISSRE) 2012, 10 pages, Dallas, TX, November 2012 (To appear)
  • J. H. Siddiqui and S. Khurshid. Scaling Symbolic Execution using Ranged Analysis. 27th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 13 pages, Tuscon, AZ, October 2012 (To appear)
  • G. Yang, S. Khurshid and M. Kim. Specification-based Test Repair Using a Lightweight Formal Method. 18th International Symposium on Formal Methods (FM), 15 pages, Paris, France, August 2012 (To appear)
  • G. Yang, C. Pasareanu, and S. Khurshid. Memoized Symbolic Execution. International Symposium on Software Testing and Analysis (ISSTA), 11 pages, Minneapolis, MN, July 2012 (To appear)
  • L. Zhang, D. Marinov, L. Zhang, and S. Khurshid. Regression Mutation Testing. International Symposium on Software Testing and Analysis (ISSTA), 11 pages, Minneapolis, MN, July 2012 (To appear)
  • J. H. Siddiqui, D. Marinov, and S. Khurshid. Lightweight Data-Flow Analysis for Execution-Driven Constraint Solving. IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), pages 91-100, Montreal, Canada, April 2012
  • M. Z. Malik and S. Khurshid. Dynamic Shape Analysis Using Spectral Graph Properties. IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), pages 211-220, Montreal, Canada, April 2012
  • J. H. Siddiqui and S. Khurshid. Staged Symbolic Execution. ACM Symposium on Applied Computing (SAC), pages 1339-1346, Riva del Garda, Italy, March 2012
  • S. A. Khalek and S. Khurshid. Efficiently Running Test Suites Using Abstract Undo Operations. IEEE 22nd International Symposium on Software Reliability Engineering (ISSRE), pages 110-119, Hiroshima, Japan, November 2011
  • L. Zhang, D. Marinov, L. Zhang, and S. Khurshid. An Empirical Study of JUnit Test-Suite Reduction. IEEE 22nd International Symposium on Software Reliability Engineering (ISSRE), pages 170-179, Hiroshima, Japan, November 2011
  • S. A. Khalek, G. Yang, L. Zhang, D. Marinov, S. Khurshid. TestEra: A tool for testing Java programs using Alloy specifications. 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 608-611, Lawrence, KS, November 2011
  • S. A. Khalek, V. P. Narayanan, and S. Khurshid. Mixed constraints for test input generation - An initial exploration. 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 548-551, Lawrence, KS, November 2011
  • S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 504-515, San Jose, CA, June 2011
  • C. Cadar, P. Godefroid, S. Khurshid, C. S. Pasareanu, K. Sen, N. Tillmann, and W. Visser. Symbolic execution for software testing in practice: Preliminary assessment. 33rd International Conference on Software Engineering (ICSE), pages 1066-1071, Waikiki, Honolulu, May 2011
  • S. A. Khalek and S. Khurshid. Systematic testing of database engines using a relational constraint solver. IEEE Fourth International Conference on Software Testing, Verification and Validation (ICST), pages 50-59, Berlin, Germany, Mar. 2011
  • C. H. P. Kim, D. S. Batory, and S. Khurshid. Reducing combinatorics in testing product lines. 10th International Conference on Aspect-Oriented Software Development (AOSD), pages 57-68, Porto de Galinhas, Brazil, Mar. 2011
  • Engin Uzuncaova, Sarfraz Khurshid, Don S. Batory. Incremental Test Generation for Software Product Lines. IEEE Transactions on Software Engineering (TSE) Volume 36, Number 3, pages 309-322, 2010
  • C. H. P. Kim, E. Bodden, D. S. Batory, and S. Khurshid. Reducing configurations to monitor in a software product line. First International Conference on Runtime Verification (RV), pages 285-299, St. Julians, Malta, Nov. 2010
  • J. H. Siddiqui and S. Khurshid. ParSym: Parallel symbolic execution. 2nd International Conference on Software Technology and Engineering (ICSTE), pages V1-405-V1-409, San Juan, PR, Oct. 2010
  • S. A. Khalek and S. Khurshid. Automated SQL query generation for systematic testing of database engines. 25th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 329-332, Antwerp, Belgium, Sept. 2010
  • C. H. P. Kim, D. S. Batory, and S. Khurshid. Eliminating products to test in a software product line. 25th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 139-142, Antwerp, Belgium, Sept. 2010
  • M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov. Test generation through programming in UDITA. 32nd ACM/IEEE International Conference on Software Engineering (ICSE), pages 225-234, Cape Town, South Africa, May 2010. (ACM SIGSOFT Distinguished Paper Award)
  • J. H. Siddiqui and S. Khurshid. An empirical study of structural constraint solving techniques. 11th International Conference on Formal Engineering Methods (ICFEM), pages 88-106, Rio de Janeiro, Brazil, 2009
  • S. R. Ganov, C. Killmar, S. Khurshid, and D. E. Perry. Event listener analysis and symbolic execution for testing GUI applications. 11th International Conference on Formal Engineering Methods (ICFEM), pages 69-87, Rio de Janeiro, Brazil, 2009
  • J. H. Siddiqui, D. Marinov, and S. Khurshid. Optimizing a Structural Constraint Solver for Efficient Software Checking. 24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009). Auckland, New Zealand. Nov 2009. Short paper.
  • J. H. Siddiqui and S. Khurshid. PKorat: Parallel generation of structurally complex test inputs. 2nd International Conference on Software Testing, Verification, and Validation (ICST 2009). Denver, CO. Apr 2009. *.pdf
  • M. Gligoric, T. Gvero, S. Lauterburg, D. Marinov, and S. Khurshid. Optimizing generation of object graphs in Java PathFinder. 2nd International Conference on Software Testing, Verification, and Validation (ICST 2009). Denver, CO. Apr 2009. *.pdf
  • X. Li, D. Shannon, I. Ghosh, M. Ogawa, S. Rajan, and S. Khurshid. Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution. 6th Asian Symposium on Programming Languages and Systems (APLAS 2008). Bangalore, India. Dec 2008. *.pdf
  • E. Uzuncaova, D. Garcia, S. Khurshid, and D. Batory. Testing Software Product Lines Using Incremental Test Generation. 19th IEEE International Symposium on Software Reliability Engineering (ISSRE 2008). Seattle, WA. Nov 2008. *.pdf
  • S. A. Khalek, B. Elkarablieh, Y. O. Laleye, and S. Khurshid. Query-aware Test Generation Using a Relational Constraint Solver. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008). L'Aquila, Italy. Sep 2008. *.pdf
  • B. Elkarablieh, D. Marinov, and S. Khurshid. Efficient solving of structural constraints. International Symposium on Software Testing and Analysis (ISSTA 2008). Seattle, WA. Jul 2008. *.pdf
  • M. Z. Malik, A. Pervaiz, E. Uzuncaova, and S. Khurshid. Deryaft: A tool for generating representation invariants of structurally complex data. 30th International Conference on Software Engineering (ICSE 2008) Research Demo Paper. Leipzig, Germany. May 2008. *.pdf
  • T. Gvero, M. Gligoric, S. Lauterburg, M. D'Amorim, D. Marinov, and S. Khurshid. State extensions for Java PathFinder. 30th International Conference on Software Engineering (ICSE 2008) Research Demo Paper. Leipzig, Germany. May 2008. *.pdf
  • S. Ganov, C. Killmar, S. Khurshild and D. Perry. Test Generation for Graphical User Interfaces Based on Symbolic Execution. Third International Workshop on Automation of Software Test (AST 2008). Leipzig, Germany. May 2008. *.pdf
  • D. Shao, S. Khurshid, and D. Perry. Whispec: White-box testing of libraries using declarative specifications. ACM SIGPLAN Symposium on Library-Centric Software Design (LCSD 2007). Montreal, Canada. Oct 2007. *.pdf
  • S. Misailovic, A. Milicevic, N. Petrovic, S. Khurshid, and D. Marinov. Parallel Test Generation and Execution with Korat. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007). Dubrovnik, Croatia. Sep 2007. *.pdf
  • E. Uzuncaova, D. Garcia, S. Khurshid, and D. Batory. A Specification-based Approach to Testing Software Product Lines. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007) Poster Paper. Dubrovnik, Croatia. Sep 2007. *.pdf
  • D. Shannon, S. Hajra, A. Lee, D. Zhan, and S. Khurshid. Abstracting Symbolic Execution with String Analysis. Testing: Academic & Industrial Conference--Practice and Research Techniques (TAIC-PART 2007). *.pdf
  • D. Shao, S. Khurshid, and D. Perry. A case for white-box testing using declarative specification. Testing: Academic & Industrial Conference--Practice and Research Techniques (TAIC-PART 2007) Poster Paper. Windsor, UK. Sep 2007. *.pdf
  • S. Ganov, S. Khurshid, and D. Perry. Symbolic execution for GUI testing. Testing: Academic & Industrial Conference--Practice and Research Techniques (TAIC-PART 2007) Poster Paper. Windsor, UK. Sep 2007. *.pdf
  • A. Milicevic, S. Misailovic, D. Marinov, and S. Khurshid. Korat: A Tool for Generating Structurally Complex Test Inputs. 29th International Conference on Software Engineering (ICSE 2007) Research Demo Paper. Minneapolis, MN. May 2007. *.pdf
  • S. Misailovic, A. Milicevic, S. Khurshid, and D. Marinov. Generating Test Inputs for Fault-tree Analyzers Using Imperative Predicates. Workshop on Advances and Innovations in System Testing. Memphis, TN. May 2007. *.pdf
  • M. Z. Malik, A. Pervaiz, and S. Khurshid. Generating Representation Invariants of Structurally Complex Data. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007). Braga, Portugal. March 2007. *.pdf
  • S. Khurshid and Y. Suen. Generalizing Symbolic Execution to Library Classes. 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2005), Lisbon, Portugal. Sep 2005. *.pdf
  • C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser and R. Washington. Combining Test Case Generation and Runtime Verification. Theoretical Computer Science (TCS), Volume 336, Issues 2-3, Pages 209-234, 26 May 2005. *.pdf
  • D. Coppit, J. Yang, S. Khurshid, W. Le, and K. Sullivan. Software Assurance by Bounded Exhaustive Testing. IEEE Transactions on Software Engineering (TSE), Volume 31, Issue 4, Pages 328-339, April 2005. (Journal version of ISSTA'2004 paper.) *.pdf
  • S. Khurshid and D. Marinov. TestEra: Specification-based Testing of Java Programs Using SAT. Automated Software Engineering Journal, Volume 11, Number 4. October 2004. (Journal version of ASE'2001 paper.) *.pdf
  • P. Godefroid and S. Khurshid. Exploring Very Large State Spaces Using Genetic Algorithms. International Journal on Software Tools for Technology Transfer (STTT), Volume 6, Number 2, pages 117-127, August 2004, Springer-Verlag. (Journal version of TACAS'2002 paper.) *.pdf
  • K. J. Sullivan, J. Yang, D. Coppit, S. Khurshid and D. Jackson. Software Assurance by Bounded Exhaustive Testing. International Symposium on Software Testing and Analysis (ISSTA 2004), Boston, MA. July 2004.*.pdf
  • W. Visser, C. S. Pasareanu, S. Khurshid: Test Input Generation with Java PathFinder. International Symposium on Software Testing and Analysis (ISSTA 2004), Boston, MA. July 2004. *.pdf
  • D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, MIT CSAIL, Cambridge, MA, September 2003. *.pdf
  • S. Khurshid, D. Marinov, I. Shlyakhter and D. Jackson. A Case for Efficient Solution Enumeration. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), S. Margherita Ligure, Portofino, Italy. May 2003. *.pdf
  • S. Khurshid, C. Pasareanu and W. Visser. Generalized Symbolic Execution for Model Checking and Testing. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2003), Warsaw, Poland. Apr 2003. *.pdf
  • C. Boyapati, S. Khurshid and D. Marinov. Korat: Automated Testing Based on Java Predicates. ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2002), Rome, Italy. Jul 2002. (This paper won an ACM SIGSOFT Distinguished Paper Award in 2002, and an ACM SIGSOFT Impact Paper Award in 2012) *.pdf
  • P. Godefroid and S. Khurshid. Exploring Very Large State Spaces Using Genetic Algorithms. 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002), Grenoble, France. Apr 2002. Lecture Notes in Computer Science (LNCS), vol. 2280, eds. J.-P. Katoen and P. Stevens, Springer-Verlag. *.pdf
  • D. Marinov and S. Khurshid. TestEra: A Novel Framework for Automated Testing of Java Programs. 16th IEEE Conference on Automated Software Engineering (ASE 2001), San Diego, CA. Nov 2001. (This paper was nominated for the best paper award by the program committee.) *.pdf
  • S. Khurshid and D. Marinov. Checking Java Implementation of a Naming Architecture Using TestEra. CAV Workshop on Software Model Checking, Paris, France. Jul 2001. Electronic Notes in Theoretical Computer Science (ENTCS), vol. 55(3), Elsevier Science. *.pdf
  • S.Khurshid and D. Marinov. Using TestEra to Check the Intentional Naming System of Oxygen (Extended Abstract). MIT Student Oxygen Workshop, Gloucester, MA. Jul 2001. *.pdf
  • S.Khurshid. Testing an Intentional Naming Scheme Using Genetic Algorithms. 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001), Genova, Italy. Apr 2001. Lecture Notes in Computer Science (LNCS), vol. 2031, eds. T. Margaria and W. Yi, Springer-Verlag. *.pdf
• Error Recovery and Automated Debugging
  • L. Zhang, M. Kim, and S. Khurshid. FaultTracer: A Change Impact and Regression Fault Analysis Tool for Evolving Java Programs. ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE), 4 pages, Research Triangle Park, NC, November 2012. Research tool demonstration paper (To appear)
  • D. Gopinath, R. N. Zaeem, and S. Khurshid. Improving the Effectiveness of Spectra-based Fault Localization using Specifications. 27th IEEE/ACM International Conference on Automated Software Engineering (ASE), 10 pages, Essen, Germany, September 2012 (To appear)
  • R. N. Zaeem, D. Gopinath, S. Khurshid, and K. S. McKinley. History-Aware Data Structure Repair Using SAT. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 2-17, Tallinn, Estonia, March 2012
  • S. Roychowdhury and S. Khurshid. Software fault localization using feature selection. International Workshop on Machine Learning Technologies in Software Engineering (MALETS), pages 11-18, Lawrence, KS, November 2011
  • S. Roychowdhury and S. Khurshid: A Novel Framework for Locating Software Faults Using Latent Divergences. European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML PKDD), pages 49-64, Athens, Greece, September 2011
  • L. Zhang, M. Kim, and S. Khurshid. Localizing failure-inducing program edits based on spectrum information. IEEE 27th International Conference on Software Maintenance (ICSM), pages 23-32, Williamsburg, VA, September 2011
  • D. Gopinath, M. Z. Malik, and S. Khurshid. Specification-based program repair using SAT. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 173-188, Saarbrucken, Germany, Mar. 2011
  • M. Z. Malik, J. H. Siddiqui, and S. Khurshid. Constraint-based program debugging using data structure repair. IEEE Fourth International Conference on Software Testing, Verification and Validation (ICST), pages 190-199, Berlin, Germany, Mar. 2011
  • R. N. Zaeem and S. Khurshid. Contract-based data structure repair using Alloy. 24th European Conference on Object-Oriented Programming (ECOOP), pages 577-598, Maribor, Slovenia, June 2010
  • R. N. Zaeem and S. Khurshid. Introducing specification-based data structure repair using Alloy. Second International Conference on Abstract State Machines, Alloy, B and Z (ABZ), pages 398-399, Orford, Canada, Feb. 2010. Abstract paper
  • M. Z. Malik, K. Ghori, B. Elkarablieh, and S. Khurshid. A Case for Automated Debugging Using Data Structure Repair. 24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009). Auckland, New Zealand. Nov 2009. Short paper. *.pdf
  • B. Elkarablieh and S. Khurshid. Juzi: A tool for repairing complex data structures. 30th International Conference on Software Engineering (ICSE 2008) Research Demo Paper. Leipzig, Germany. May 2008. *.pdf
  • B. Elkarablieh, I. Garcia, Y. Suen, and S. Khurshid. Assertion-based Repair of Complex Data Structures. 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007). Atlanta, GA. Nov 2007. *.pdf
  • B. Elkarablieh, S. Khurshid, D. Vu, and K. McKinley. STARC: Static Analysis for Efficient Repair of Complex Data. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2007). Montreal, Canada. Oct 2007. *.pdf
  • B. Elkarablieh, Y. Zayour, S. Khurshid. Efficiently Generating Structurally Complex Inputs with Thousands of Objects. 21st European Conference on Object-Oriented Programming (ECOOP 2007). Berlin, Germany. Aug 2007. *.pdf
  • S. Khurshid, I. Garcia and Y. Suen. Repairing Structurally Complex Data. 12th International SPIN Workshop on Model Checking of Software (SPIN 2005), San Francisco, CA. Aug 2005. *.pdf
• Object Modeling and Static Analysis
  • S. Ganov, S. Khurshid, and D. E. Perry. Annotation-aided Automated Incremental Analysis for Alloy via Domain Specific Solvers. 14th International Conference on Formal Engineering Methods (ICFEM), 16 pages, Kyoto, Japan, November 2012 (To appear)
  • S. R. Ganov, S. Khurshid, and D. E. Perry. A case for Alloy annotations for efficient incremental analysis via domain specific solvers. 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 464-467, Lawrence, KS, November 2011
  • J. H. Siddiqui and S. Khurshid. Symbolic Execution of Alloy Models. 13th International Conference on Formal Engineering Methods (ICFEM), pages 340-355, Durham, UK, October 2011
  • D. Shao, D. Gopinath, S. Khurshid, and D. E. Perry. Optimizing incremental scope-bounded checking with data-flow analysis. IEEE 21st International Symposium on Software Reliability Engineering (ISSRE), pages 408-417, San Jose, CA, Nov. 2010
  • D. Shao, D. Gopinath, S. Khurshid, and D. E. Perry. A case for using data-flow analysis to optimize incremental scope-bounded checking. Second International Conference on Abstract State Machines, Alloy, B and Z (ABZ), pages 392-393, Orford, Canada, Feb. 2010. Abstract paper
  • D. Shao, S. Khurshid and D. Perry. An incremental approach to scope-bounded checking using a lightweight formal method. 6th International Symposium on Formal Methods (FM 2009). Eindhoven, the Netherlands. Nov 2009. *.pdf
  • E. Uzuncaova and S. Khurshid. Constraint prioritization for efficient analysis of declarative models. 15th International Symposium on Formal Methods (FM 2008). Turku, Finland. May 2008. *.pdf
  • F. Zaraket, A. Aziz, and S. Khurshid. Sequential Circuits for Program Analysis. 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007). Atlanta, GA. Nov 2007. *.pdf
  • F. Zaraket, J. Pape, M. Jacome, A. Aziz, and S. Khurshid. Global Optimization of Compositional Systems. International Confrence on Formal Methods in Computer Aided Design (FMCAD 2007). Austin, TX. Nov 2007. *.pdf
  • R. Podorozhny, S. Khurshid, D. Perry, X. Zhang. Verification of Multi-agent Negotiations Using the Alloy Analyzer. iFM 2007: integrated Formal Methods. Oxford, UK. July 2007. *.pdf
  • F. Zaraket, A. Aziz, and S. Khurshid. Sequential Circuits for Relational Analysis. 29th International Conference on Software Engineering (ICSE 2007). Minneapolis, MN. May 2007. *.pdf
  • E. Uzuncaova and S. Khurshid. Kato: A Program Slicing tool for Declarative Specifications. 29th International Conference on Software Engineering (ICSE 2007) Research Demo Paper. Minneapolis, MN. May 2007. *.pdf
  • E. Uzuncaova and S. Khurshid. Program Slicing for Declarative Specifications. 14th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE 2006) Poster Paper. Portland, OR. November 2006. *.pdf
  • F. Zaraket, A. Aziz, and S. Khurshid. Applying a Sequential Circuit Solver to Alloy. First Alloy Workshop (Alloy 2006). Portland, OR. November 2006. PDF of workshop proceedings
  • D. Marinov and S. Khurshid. What Will the User Do (Next) in the Tool? First Alloy Workshop (Alloy 2006). Portland, OR. November 2006. PDF of workshop proceedings
  • C. Chen, P. Grisham, S. Khurshid and D. Perry. Design and Validation of a General Security Model with the Alloy Analyzer. First Alloy Workshop (Alloy 2006). Portland, OR. November 2006. PDF of workshop proceedings
  • S. Khurshid, M. Z. Malik, and E. Uzuncaova. Generating Alloy Specifications from Instances. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006). Paphos, Cyprus. November 2006. *.pdf
  • X. Li, D. Shannon, J. Walker, S. Khurshid, and D. Marinov. Characterizing the Uses of a Software Modeling Tool. 6th Workshop on Language Descriptions, Tools and Applications (LDTA 2006), Vienna, Austria. Apr 2006. *.pdf
  • D. Marinov, S. Khurshid, S. Bugrara, L. Zhang, and M. Rinard. Optimizations for Compiling Declarative Models into Boolean Formulas. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), St. Andrews, Scotland. Jun 2005. *.pdf
  • S. Khurshid, D. Marinov and D. Jackson. An Analyzable Annotation Language. 17th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2002), Seattle, WA. Nov 2002. *.pdf
  • D. Marinov and S. Khurshid. VAlloy: Virtual Functions Meet a Relational Language. 11th International Symposium of Formal Methods Europe (FME 2002), Copenhagen, Denmark. Jul 2002. *.pdf
  • S. Khurshid and D. Jackson. Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer. 15th IEEE International Conference on Automated Software Engineering (ASE 2000), Grenoble, France. Sep 2000. *.pdf
  • S. Khurshid. Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer. S.M. Thesis. Laboratory for Computer Science, M.I.T. Cambridge, MA. May 2000.
• Parallel Development and Requirements
  • D. Shao, S. Khurshid, and D. Perry. SCA: a Semantic Conflict Analyzer for Parallel Changes. 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2009). Demonstrations Track Paper. Amsterdam, the Netherlands. Nov 2009. *.pdf
  • D. Shao, S. Khurshid, D. Perry. Semantic Impact and Faults in Source Code Changes: An Empirical Study. 20th Australian Software Engineering Conference (ASWEC 2009). Gold Coast, Australia. Apr 2009. (This paper won the best research paper award.) *.pdf
  • D. Shao, S. Khurshid, and D. Perry. Integrating semantic interference detection into version management systems. 2nd Workshop on Accountability and Traceability in Global Software Engineering (ATGSE 2008). Beijing, China. Dec 2008 *.pdf
  • F. Ahmed, Q. Durrani, and S. Khurshid. Exploring traceability-based requirements inspection. International Conference on Software Engineering and Applications (SEA 2007). Boston, MA. Nov 2007.
  • D. Shao, S. Khurshid, and D. Perry. Evaluation of Semantic Interference Detection in Parallel Changes: an Exploratory Experiment. 23rd Inernational Conference on Software Maintenance (ICSM 2007). Paris, France. Oct 2007. *.pdf
• Theorem Proving
  • A. Spiridonov and S. Khurshid. Pythia: Automatic generation of counterexamples for ACL2 using Alloy. Seventh International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2007). Austin, TX. Nov 2007. *.pdf
  • K. Arkoudas, S. Khurshid, D. Marinov, and M. Rinard. Integrating model checking and theorem proving for relational reasoning. 7th International Seminar on Relational Methods in Computer Science (RelMiCS 7), Malente, Germany. May 2003. *.pdf
• Semantics
  • S. Drossopoulou, S. Eisenbach and S. Khurshid. Is the Java Type System Sound? Theory and Practice of Object Systems, Volume 5(1), pp. 3-24, 1999, John Wiley & Sons. download