Current Position

Research Interest

• Application of formal methods to the design, specification, and verification of general-purpose and special purpose programming languages and their implementation.
• Applications of process algebras and type systems to communication and security.
• Formal methods and software engineering support for formal specification and analysis of computer systems with human operators.

Education

Professional Experience

• January 2015 to Present: Research Professor and Senior Lecturer. Department of Computer Science, University of Illinois at Urbana-Champagne.
• August 2004 to January 2015: Research Associate Professor and Senior Lecturer. Department of Computer Science, University of Illinois at Urbana-Champaign.
• August 2000 to July 2004: Associate Professor, Department of Computer Science, New Jersey Institute of Technology.
• October 1996 to July 2000: Member of Technical Staff, Bell Laboratories, Lucent Technologies.
• April 1990 to September 1996: Member of Technical Staff, Bell Laboratories, AT&T.
• October 1987 to March 1990: Post-Doctoral Research Assistant, University of Pennsylvania.
• November 1986 to June 1987: Research Assistant, University of Cambridge Computer Laboratory.

Funding at UIUC
The folowing is a listing of the grants and contracts I have held while at UIUC, listed in reverse chronological order. Several of these where multi-institutional grants. I will use PI to indicate the Principal Investigator at each institution, Lead PI for the PI at the lead institution, and Co-PI for co-Principal Investigators. I have not listed funding that I transfered to UIUC when I came.

• “REU:SHF:Small:A Verification Framework for Optimization of Parallel Programs and Program Transformation (VeriF-OPT)”, NSF, $16,000, 2013-2014, (PI) Elsa L. Gunter, (Co-PI) Grigore Roşu.
• “SHF:Small:A Verification Framework for Optimization of Parallel Programs and Program Transformation (VeriF-OPT)”, NSF, $450,000, 2013-2016, (PI) Elsa L. Gunter, (Co-PI) Grigore Roşu.
• “Trust from Explicit Evidence: Integrating Digital Signatures and Formal Proofs”, Dept. of Defense through ITI Lablet on Security, $150,000, 2012-2014, (PI) Elsa L. Gunter.
• “NextGenAA: Integrated Model Checking and Simulation of NextGen Authority and Autonomy”, NASA, $2,533,574 - $652,025 at UIUC, 2010-2013, (Lead PI, UVa, Drexel) Ellen Bass, (PI GA Tech) Karen Feigh, (PI) Elsa L. Gunter.
• “Formalizing Operator Task Analysis”, NSF, $500,00, 2009-2011, (PI) Elsa L. Gunter, (Co-PI) Carl Gunter.
• “ITR: Secure Electronic Transactions”, NSF (subcontracted through Stevens Institute of Technology), $179,312, (Lead PI, Stevens) Adriana Compagnoni, (PI at UIUC) Elsa L. Gunter.
• “Advanced Tool Integration for Embedded System Assurance”, ARO MURI, $191,885 at UIUC, transferred from NJIT, (PI at UIUC) Elsa L. Gunter

Patents

• “An Interactive Software Testing System And Method,” joint with Doron Peled, submitted Sept. 3, 1998, issued June 2002, Patent Number 6,408,430.

Awards

• Most Influential 10 Year Paper award at Requirements Engineering (RE 2010). Joint with Carl A. Gunter, Michael Jackson, and Pamela Zave.
• EASST (European Association of Software Science and Technology) Best Software Science Paper presented at the European Joint Conference on Theory and Practice of Software (ETAPS) 2001, April 2-6, Genova, Italy.
• Best paper award for paper in Fourth International Conference on Requirements Engineering, June 2000, Schaumberg IL. Joint with Carl A. Gunter, Michael Jackson, and Pamela Zave.

Invited Talks

• “Mobile Access Control”: Symposium on Trustworthy Global Computing (TGC 2005). Joint work with Adriana Compagnoni. Edinburgh, UK, April 7–9, 2005.
• “Mobile Access Control”: Stevens, Columbia and IBM Security and Privacy Day. Joint work with Adriana Compagnoni. Hoboken, NJ, November 14, 2005.

Publications

Journal Articles

1. [ECEASST2001] Ellen J. Bass, Karen M. Feigh, Elsa L. Gunter, John M. Rushby: “Formal Modeling and Analysis for Interactive Hybrid Systems.” ECEASST 45 (2011)
2. [TCS2008] Adriana B. Compagnoni, Elsa L. Gunter, Philippe Bidinger: “Role-based access control for boxed ambients.” Theor. Comput. Sci. 398(1-3): 203-216 (2008)
3. [ENTCS2005] Eduardo Bonelli, Adriana B. Compagnoni, Elsa L. Gunter: “Typechecking Safe Process Synchronization.” Electr. Notes Theor. Comput. Sci. 138(1): 3-22 (2005)
4. [FAC2005] Elsa L. Gunter, Doron Peled: “Model checking, testing and verification working together.” Formal Asp. Comput. 17(2): 201-221 (2005)
5. [JFP2005] Eduardo Bonelli, Adriana B. Compagnoni, Elsa L. Gunter: “Correspondence assertions for process synchronization in concurrent communications.” J. Funct. Program. 15(2): 219-247 (2005)
6. [ENTCS2004] Eduardo Bonelli, Adriana B. Compagnoni, Elsa L. Gunter: “Correspondence Assertions for Process Synchronization in Concurrent Communications.” Electr. Notes Theor. Comput. Sci. 97: 175-195 (2004)
7. [STTT2004] Rajeev Alur, David Arney, Elsa L. Gunter, Insup Lee, Jaime Lee, Wonhong Nam, Frederick Pearce, Stephen Van Albert, Jiaxiang Zhou: “Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System.” STTT 5(4): 308-319 (2004)
8. [STTT2003] Elsa L. Gunter, Anca Muscholl, Doron Peled: “Compositional message sequence charts.” STTT 5(1): 78-89 (2003)
9. [ENTCS2002] Elsa L. Gunter, Doron Peled: “Tracing the executions of concurrent programs.” Electr. Notes Theor. Comput. Sci. 70(4): 128-141 (2002)
10. [SIGSOFT2000] Carl A. Gunter, Elsa L. Gunter, Pamela Zave: “Formal software engineering.” ACM SIGSOFT Software Engineering Notes 25(1): 54 (2000)
11. [IEEESoftware2000] Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Pamela Zave: A Reference Model for Requirements and Specifications. IEEE Software 17(3): 37-43 (2000)
12. [CJ1995] Elsa L. Gunter, Savi Maharaj: “Studying the ML Module System in HOL.” Comput. J. 38(2): 142-151 (1995)
13. [IC1992] Carl A. Gunter, Elsa L. Gunter, David B. MacQueen: “Computing ML Equality Kinds Using Abstract Interpretation.” Inf. Comput. 107(2): 303-323 (1993)
    
    Book Chapter
14. Elsa L. Gunter. “HOL case study: Modular arithmetics.” In The HOL System: Tutorial, Volume 2, chapter 9: 233-345. Michael J. C. Gordon, editor. Cambridge Research Centre, SRI International. (1989)
    
    Edited Conference Proceedings
15. Elsa L. Gunter, Amy P. Felty (Eds.): “Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97”, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings. Lecture Notes in Computer Science 1275, Springer 1997, ISBN 3-540-63379-0
    
    Refereed Conference and Workshop Papers
16. [ICTAC2014] Liyi Li, Elsa Gunter and William Mansky: “Symbolic Analysis Tools for CSP.” Eleventh International Colloquium on Theoretical Aspects of Computing 2014: to appear
17. [LOLA2014] William Mansky and Elsa Gunter: “A Cross-Language Framework for Verifying Compiler Optimizations.” Fifth Workshop on Syntax and Semantics of Low-Level Languages: to appear
18. [WPTE2014] William Mansky and Elsa Gunter: “Verifying Optimizations for Concurrent Programs.” Workshop on Rewriting Techniques for Program Transformations and Evaluation 2014.: to appear
19. [GRAPHITE2014] William Mansky, Dennis Griffith and Elsa Gunter: “Specifying and Executing Optimizations for Parallel Programs.” 3rd Workshop On GRAPH Inspection and Traversal Engineering: to appear
20. [NFM2013] Dennis Griffith, Elsa L. Gunter: “LiquidPi: Inferrable Dependent Session Types.” NASA Formal Methods 2013: 185-197
21. [ATACCS2012] Ayesha Yasmeen, Karen M. Feigh, Gabriel Gelman, Elsa L. Gunter: “Formal analysis of safety-critical system simulations.” ATACCS 2012: 71-81
22. [ITP2012] William Mansky, Elsa L. Gunter: “Using Locales to Define a Rely-Guarantee Temporal Logic.” ITP 2012: 299-314
23. [ICFP2011] Andrei Popescu, Elsa L. Gunter: “Recursion principles for syntax with bindings and substitution.” ICFP 2011: 346-358
24. [ISSTA2011] Ayesha Yasmeen, Elsa L. Gunter: “Automated framework for formal operator task analysis.” ISSTA 2011: 78-88
25. [SMC2011a] Ayesha Yasmeen, Elsa L. Gunter: “Robustness for protection envelopes with respect to human task variation.” SMC 2011: 1809-1816
26. [SMC2011b] Ellen J. Bass, Matthew L. Bolton, Karen M. Feigh, Dennis Griffith, Elsa L. Gunter, William Mansky, John M. Rushby: “Toward a multi-method approach to formalizing human-automation interaction and human-human communications.” SMC 2011: 1817-1824
27. [FOSSACS2010] Andrei Popescu, Elsa L. Gunter: “Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization.” FOSSACS 2010: 109-127
28. [ITP2010] William Mansky, Elsa L. Gunter: “A Framework for Formal Verification of Compiler Optimizations.” ITP 2010: 371-386
29. [LICS2010] Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn: “Strong Normalization for System F by HOAS on Top of FOAS”. LICS 2010: 31-40
30. [HICSS2009] Elsa L. Gunter, Ayesha Yasmeen, Carl A. Gunter, Anh Nguyen: “Specifying and Analyzing Workflows for Automated Identification and Data Capture.” HICSS 2009: 1-11
31. [LFMTP2009] Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu: “Theory support for weak higher order abstract syntax in Isabelle/HOL.” LFMTP 2009: 12-20
32. [FAST2008] Elsa L. Gunter, Ayesha Yasmeen: “Secure Broadcast Ambients.” Formal Aspects in Security and Trust 2008: 257-271
33. [RTSS2007] Tanya L. Crenshaw, Elsa L. Gunter, Craig L. Robinson, Lui Sha, P. R. Kumar: “The Simplex Reference Model: Limiting Fault-Propagation Due to Unreliable Components in Cyber-Physical System Architectures.” RTSS 2007: 400-412
34. [HCMDSS2007] Jennifer Hou, Qixin Wang, Linda Ball, Stanley Birge, Marco Caccamo, Chin-Fei Cheah, Eric Gilbert, Carl Gunter, Elsa Gunter, Chang-Gun Lee, Karrie Karahalios, Min-Young Nam, Narasimhan Nitya, Chaudhri Rohit and Lui Sha: “PAS: A Wireless-enabled, Sensor-integrated Personal Assistance System for Independent and Assisted Living.” High Confidence Medical Devices, Software, and Systems and Medical Device Plug-and-Play Interoperability, 2007. (HCMDSS-MDPnP 2007).: 64-75
35. [SMC2006] Qixin Wang, Wook Shin, Xue Liu, Zheng Zeng, Cham Oh, Bedoor K. AlShebli, Marco Caccamo, Carl A. Gunter, Elsa L. Gunter, Jennifer C. Hou, Karrie Karahalios, Lui Sha: “I-Living: An Open System Architecture for Assisted Living.” SMC 2006: 4268-4275
36. [TGC2005] Adriana B. Compagnoni, Elsa L. Gunter: “Types for Security in a Mobile World.” TGC 2005: 75-97
37. [VTP2003] Elsa L. Gunter, Doron Peled: “Unit Checking: Symbolic Model Checking for a Unit of Code.” Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 2003: 548-567
38. [TACAS2002] Elsa L. Gunter, Doron Peled: “Temporal Debugging for Concurrent Systems.” TACAS 2002: 431-444
39. [TACAS2001] Elsa L. Gunter, Anca Muscholl, Doron Peled: “Compositional Message Sequence Charts.” TACAS 2001: 496-511
40. [CAV2000] Elsa L. Gunter, Robert P. Kurshan, Doron Peled: “PET: An Interactive Software Testing Tool.” CAV 2000: 552-556
41. [ICRE2000] Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Pamela Zave: “A Reference Model for Requirements and Specifications-Extended Abstract.” ICRE 2000: 189
42. [PDPTA2000] Elsa L. Gunter, Doron Peled: “Using a Mix of Languages in Formal Methods: The PET System.” PDPTA 2000
43. [TACAS1999] Elsa L. Gunter, Doron Peled: “Path Exploration Tool.” TACAS 1999: 405-419
44. [TPHOLs1998a] Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave: “The Village Telephone System: A Case Study in Formal Software Engineering.” TPHOLs 1998: 49-66
45. [TPHOLs1998b] Elsa L. Gunter: “Adding External Decision Procedures to HOL90 Securely.” TPHOLs 1998: 143-152
46. [HOL1995] Elsa L. Gunter, Leonid Libkin: “Interfacing HOL90 with a Functional Database Query Language.” HOL 1995: 170-185
47. [DEXA1994] Elsa L. Gunter, Leonid Libkin: “OR-SML: A Functional Database Programming Language for Disjunctive Information and Its Applications.” DEXA 1994: 641-650
48. [HOL1994] Savi Maharaj, Elsa L. Gunter: “Studying the ML Module System in Hol.” HOL 1994: 346-361
49. [HUG1993a] Myra Van Inwegen, Elsa L. Gunter: “HOL-ML.” HUG 1993: 61-74
50. [HUG1993b] Elsa L. Gunter: “A Broader Class of Trees for Recursive Type Definitions for HOL.” HUG 1993: 141-154
51. [HOL1992] Elsa L. Gunter: “Why we can’t have SML-style datatype Declarations in HOL.” HOL 1992: 561-568
52. [TACS1991] Carl A. Gunter, Elsa L. Gunter, David B. MacQueen: “An Abstract Interpretation for ML Equality Kinds.” TACS 1991: 112-130
53. [HOL1991] Richard Gerber, Elsa L. Gunter, Insup Lee: “Implementing a Real-Time Process Algebra in HOL.” HOL 1991: 144-154
54. [CADE1990] Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning: “Tutorial on Lambda-Prolog.” CADE 1990: 682
55. [ELP1989] Elsa L. Gunter: “Extensions to Logic Programming Motivated by the Construction of a Generic Theorem Prover.” ELP 1989: 223-244
56. [MFPS1989] Elsa L. Gunter: “Pseudo-Retract Functors for Local Lattices and Bifinite L-domains.” Mathematical Foundations of Programming Semantics 1989: 351-363
57. [CADE1988] Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov: “Lambda-Prolog: An Extended Logic Programming Language.” CADE 1988: 754-755

Systems Design and Implementation:

• DSILL a distributed and parallel functional language with communication across channels with linear logic session types. Based on the language SILL by Frank Pfenning. Joint work with Dennis Griffith.
• VeriF-OPT A Verification Framework for Optimizations and (Parallel) Program Transformations, combining the abstract semantics of the parallel-language transformation language PTRANS
• PTRANS Executable Semantics for specifying and testing optimizations as CTL-conditioned graph rewrites on low-level parallel code expressed using control-flow graphs. Joint with William Mansky.
• Tutela for modeling combined machine and human operator systems, and for determining how much protection a computer system has against possible (un)predictable human operator action variations. Joint work with Ayesha Yasmeen.
  • Tutela Example: Analysis of a self-scan checkout system for the robustness of operator requirements deviation.
• Simulation Trace Verifier for verifying LTL properties of simulation traces produced by the simulator Work Models that Compute (WMC) from Georgia Tech, via the reduction, abstraction, augmentation and conversion to finite state machines of the traces. Joint work with Ayesha Yasmeen. https://wiki.engr.illinois.edu/display/fmvl/Formal+Verification+of+Simulation+Traces
• DOVE extension for composing extended finite state machines to enable modular reasoning about concurrent systems. Joint work with Yi Meng.
• PET, the Path Evaluation Tester, a tool for the selection and analysis of paths in concurrent programs. Joint with Doron Peled.
• HOL90 Higher-order logic theorem prover based on HOL88 developed at Cambridge University. Work joint with Konrad Slind when he interned as a Master’s student at Bell Labs. This system was has been the basis of dozens of projects, and used by hundreds of users (over 400 users downloaded HOL90 version 7). It formed the basis of the interactive theorem provers HOL4 and HOL-Light, and was influential in the creation of the Isabelle-HOL.

Student Supervisions:
Graduated Ph.D. Students

• William Mansky: “Specifying and Verifying Program Transformations with PTRANS,” April 2014. Current Position: Post-doc at the University of Pennsylvania.
• Ayesha Yasmeen: “Formalizing Operator Task Analysis,” June 2011. Current Position: Software Engineer at Turn.
• Andrei Popescu: “Contributions to the Theory of Syntax with Bindings and to Process Algebra,” October 2010. Current Position: Post-doc at the Informatics Institute, Technical University Munich.
• Yi Meng: “Automata-based Automatic Software Verification Framework,” May 2006, NJIT. No record of his current position, may have returned to China.
  
  Current Ph.D. Students
• Dennis Griffith: “Lightweight Secure Distributed Programming.” Expected completion: December 2015.
• Susannah Johnson: “Formal Framework for Access Control Evaluation.” Expected completion: May 2019.
• Liyi Li, co-advised by Prof. Grigore Roşu. General topic – formalisms and tool support for concurrent languages. Expected completion: May 2018.
  
  Graduated M.S. Students
• Liyi Li, UIUC 2014
• Christopher J. Osborn, UIUC 2010
• Justin S. Davis, UIUC 2006
• Hassan Adekoya, NJIT 2003
• Swaroop Malangi, NJIT 2003
• Dhruv Kataria, NJIT 2002
• Guhan Swaminathan, NJIT 2002
  
  Graduated B.S. Thesis Students
• Kyungwha Byun, May 2014
• Matthew L. Cooper, May 2014
• Ryan M. Hitchman, May 2014
• John J. Lee, May 2014
• Liyi Li, May 2012
• Eric C. Peterson, May 2009
• James B. Kionka, May 2008
  
  Thesis Committee Non-Advisor Member
• Brandon Moore – Prelim: Dec 12, 2013, Thesis Defense, expected Spring 2015
• Tanya Crenshaw – Prelim: November 15, 2007; Thesis Defense: July 18, 2008
  
  Other Academic Supervisions
• Ph.D. students supervised while at Bell Labs for summer projects, or fellowships: Vijay Gehlot, Savitri Maharaj, Diana Meadows, Ramesh Subramaniam, Myra VanInwegen, Healfdene Goguen, Leonid Libkin, Mark Smith, Davor Obradovic, Karthikeyan Bhargavan
• Other students supervised at Bell Labs: Konrad Slind (MS student), Rafael Hernandez (BS).

External Reviewing
Program Committees:

• AAAI 2014 Spring Symposium on Formal Verification & Modeling in Human-Machine Systems FVHMS-2014;
• First through Fifth International Conference on Interactive Theorem Proving (2010 - 2014);
• International Workshop on Logical Frameworks and Meta-languages: Theory and Practice LFMTP 2012, 2014;
• Programming Methods for Mobile and Pervasive Systems, PMMPS 2010, 2011;
• Workshop on Mechanized Metatheory, WMM 2010;
• Monterey Workshop (2003);
• Ninth through Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs’96 - TPHOLs’08);
• Chair of the Tenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs’97);
• Seventh and Eighth International Workshop on Higher Order Logic Theorem Proving and its Applications (1994, 1995)
• Twelfth Conference on Automated Deduction (CADE 1994);
• Lambda Prolog Workshop (1992);
• Fourth and Fifth Annual HOL Users Meeting (1991, 1992);
  
  Proposal and Project Reviews
• NSF Panel 2004, 2005, 2008, 2009, 2014
• Member of NSF workshop on the future of automated deduction (1996)
• Member of an external review board for the Formal Methods department at TeleDanmark (1994);