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; error recovery; 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) and the Naval Undersea Warfare Center.

Community

• 2009: OOPSLA PC, ICST PC, SPIN PC, ICSE Research Demo Track PC
• 2008: ISSTA PC, ASE ERP, SPIN PC, ICST student track PC, FACS PC
• 2007: ASE ERP, IWLU (ASE Workshop) PC
• 2006: ASE PC, Poster Track PC, SOQUA (FSE Workshop) PC, Alloy (FSE Workshop) PC
• 2005: SPIN PC, ICSE Research Demo Track PC
• 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), Spring 2008 (Option III), 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.)
• EE360C Algorithms, Fall 2008. (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
  • Vidya Narayanan
• Undergraduate
  Niyantha Shekar
• 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.)
  • Christopher Tsai (Undergraduate Researcher. 2007.)

Research

• Software Testing and Model Checking
  • 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. (To Appear.)
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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).
  • 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.
  • 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.
  • 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
• Data Structure Repair
  • 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.
  • 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.
  • 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.
  • 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
  • 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.
  • 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.
  • 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.
  • 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.
• Requirements and Parallel Development
  • 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.
• 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.
  • 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

Resume (12/12/2002, outdated!)