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 Assistant Professor of Electrical and Computer Engineering at UT Austin in the Center for Excellence in Distributed Global Environments (EDGE). 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: static and dynamic checking of code conformance; software testing; model checking; formal specification languages; and applications of AI-based heuristics to program analysis.

My research is funded in part by the National Science Foundation (awards CCF-0702680 and IIS-0438967).

Resume (12/12/2002)

Community

• International Symposium on Software Testing and Analysis (ISSTA 2008) Program Committee
• Automated Software Engineering (ASE 2008) Expert-Review Panel
• SPIN Workshop on Model Checking of Software (SPIN 2008) Program Committee
• Automated Software Engineering (ASE 2007) Expert-Review Panel
• ASE Workshop: Living with Uncertainties (IWLU 2007) Program Committee
• Foundations of Software Engineering (FSE 2006) Poster Session Committee
• FSE 2006 Workshop: Software Quality Assurance (SOQUA 2006) Program Committee
• FSE 2006 Workshop: Alloy 2006 Program Committee
• HICSS-40 Minitrack: Automated Software Testing and Analysis: Techniques, Practices and Tools Program Committee
• Automated Software Engineering (ASE 2006) Program Committee
• SPIN Workshop on Model Checking of Software (SPIN 2005) Program Committee
• International Conference on Software Engineering (ICSE 2005) Demo Session Committee
• National Science Foundation Panel

Teaching

• 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). (Accessible via UT's blackboard system.)
• EE322C Data Structures, Spring 2005, Spring 2006, Spring 2007. (Accessible via UT's blackboard system.)
• EE379K Software Testing, Fall 2006. (Accessible via UT's blackboard system.)

Students

• Doctoral
  • Bassem Elkarablieh
  • Junaid Haroon
  • Daryl Shannon
  • Danhua Shao (co-supervised with Dewayne Perry)
  • Engin Uzuncaova
• Masters
  • Shadi Abdul Khalek
• Undergraduate
  • Christopher Tsai
• Former (Masters)
  • Ivan Garcia (M.S. May 2005.)
  • Yuk Lai Suen (M.S. May 2005.)
  • Khalid Ghori (M.S. August 2006.)
  • Daniel Garcia (M.S. December 2006.)
  • Alison Lee (M.S. May 2007.)
  • Muhammad Younas (M.S. August 2007.)
  • Lavanya Chockalingam (M.S. December 2007.)
  • Amresh Kulkarni (M.S. December 2007.)
  • Muhammad Zubair Malik (M.S. December 2007.)
  • Daiqian Zhan (M.S. December 2007.)
• Former (Undergraduate)
  • Michael Lin (Undergraduate Researcher. Summer 2005.)
  • Sonik Shah (Undergraduate Researcher. 2007.)

Research

• Data Structure Repair
  • 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. (To appear.)
  • 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. (To appear.)
  • 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
• Software Testing and Model Checking
  • 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). (To appear.)
  • 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. (To appear.)
  • 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). (To appear.)
  • 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) *.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
• Object Modeling and Static Analysis
  • 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. (To appear.)
  • 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.
  • D. Marinov and S. Khurshid. What Will the User Do (Next) in the Tool? First Alloy Workshop (Alloy 2006). Portland, OR. November 2006.
  • 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.
  • 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.
  • 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
  • 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. (To appear.)
• Theorem Proving
  • 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