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 of Electrical and Computer Engineering at UT 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: static and dynamic checking of code conformance; software testing; repair of structurally complex data; model checking; formal specification languages; parallel and incremental algorithms for software analysis.

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.

Community

• 2012: ABZ: Alloy track PC Chair, FM PC, FSE PC, ICST PC, Regression 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 Panel

Students (Current)

• Doctoral
  • Shadi Abdul Khalek (M.S. (Thesis) May 2009.)
  • Muhammad Zubair Malik (M.S. (Thesis) December 2007.)
  • Daryl Shannon (M.S. (Report). May 2005.)
  • Danhua Shao (co-supervised with Dewayne Perry)
  • Junaid Haroon Siddiqui
• Masters
  • Divya Gopinath
  • Sowmiya Narayanan
  • Vidya Narayanan
  • Razieh Nokhbeh Zaeem
• Undergraduate
  Niyantha Shekar

Students (Former)

• Doctoral
  • Engin Uzuncaova (Ph.D. December 2008. Now working at Microsoft.)
  • Bassem Elkarablieh (Ph.D. May 2009. Now working at Google.)
• Masters (Thesis option)
  • 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.)
  • Daiqian Zhan (M.S. December 2007.)
• Undergraduate
  • Michael Lin (Undergraduate Researcher. Summer 2005.)
  • Sonik Shah (Undergraduate Researcher. 2007.)
  • Christopher Tsai (Undergraduate Researcher. 2007.)

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

Research

• Software Testing, Symbolic Execution, and Model Checking
  • 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. (To appear.)
  • 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) *.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
  • 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
  • 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. (To appear.) *.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. (To appear.) *.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