Elsa L. Gunter
Curriculum Vitae
June 2015

Current Position

Research Professor and Senior Lecturer
Department of Computer Science, University of Illinois at Urbana-Champaign
Siebel Center, 201 N. Goodwin, Urbana, IL 61801-2302

Research Interest


University of Chicago, Mathematics,B.A., June 1979
University of Wisconsin, Madison,Mathematics,M.A., May 1981
University of Wisconsin, Madison,Mathematics,Ph.D.,January 1987

Professional Experience

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.



Invited Talks


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:

Student Supervisions:
Graduated Ph.D. Students

External Reviewing
Program Committees: