Elsa L Gunter Publications

Formal Methods in Programming Languages

• [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
• [WPTE2014] William Mansky and Elsa Gunter: “Verifying Optimizations for Concurrent Programs.” Workshop on Rewriting Techniques for Program Transformations and Evaluation 2014.: to appear
• [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
• [ICFP2011] Andrei Popescu, Elsa L. Gunter: “Recursion principles for syntax with bindings and substitution.” ICFP 2011: 346-358
• [FOSSACS2010] Andrei Popescu, Elsa L. Gunter: “Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization.” FOSSACS 2010: 109-127
• [ITP2010] William Mansky, Elsa L. Gunter: “A Framework for Formal Verification of Compiler Optimizations.” ITP 2010: 371-386
• [LICS2010] Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn: “Strong Normalization for System F by HOAS on Top of FOAS”. LICS 2010: 31-40
• [LFMTP2009] Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu: “Theory support for weak higher order abstract syntax in Isabelle/HOL.” LFMTP 2009: 12-20
• [FAC2005] Elsa L. Gunter, Doron Peled: “Model checking, testing and verification working together.” Formal Asp. Comput. 17(2): 201-221 (2005)
• [STTT2003] Elsa L. Gunter, Anca Muscholl, Doron Peled: “Compositional message sequence charts.” STTT 5(1): 78-89 (2003)
• [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
• [ENTCS2002] Elsa L. Gunter, Doron Peled: “Tracing the executions of concurrent programs.” Electr. Notes Theor. Comput. Sci. 70(4): 128-141 (2002)
• [TACAS2002] Elsa L. Gunter, Doron Peled: “Temporal Debugging for Concurrent Systems.” TACAS 2002: 431-444
• [TACAS2001] Elsa L. Gunter, Anca Muscholl, Doron Peled: “Compositional Message Sequence Charts.” TACAS 2001: 496-511
• [CAV2000] Elsa L. Gunter, Robert P. Kurshan, Doron Peled: “PET: An Interactive Software Testing Tool.” CAV 2000: 552-556
• [PDPTA2000] Elsa L. Gunter, Doron Peled: “Using a Mix of Languages in Formal Methods: The PET System.” PDPTA 2000
• [TACAS1999] Elsa L. Gunter, Doron Peled: “Path Exploration Tool.” TACAS 1999: 405-419
• [HOL1994] Savi Maharaj, Elsa L. Gunter: “Studying the ML Module System in Hol.” HOL 1994: 346-361
• [HUG1993a] Myra Van Inwegen, Elsa L. Gunter: “HOL-ML.” HUG 1993: 61-74
• [HUG1993b] Elsa L. Gunter: “A Broader Class of Trees for Recursive Type Definitions for HOL.” HUG 1993: 141-154
• [HOL1992] Elsa L. Gunter: “Why we can’t have SML-style datatype Declarations in HOL.” HOL 1992: 561-568
• [TACS1991] Carl A. Gunter, Elsa L. Gunter, David B. MacQueen: “An Abstract Interpretation for ML Equality Kinds.” TACS 1991: 112-130
• [CJ1995] Elsa L. Gunter, Savi Maharaj: “Studying the ML Module System in HOL.” Comput. J. 38(2): 142-151 (1995)
• [HOL1995] Elsa L. Gunter, Leonid Libkin: “Interfacing HOL90 with a Functional Database Query Language.” HOL 1995: 170-185
• [DEXA1994] Elsa L. Gunter, Leonid Libkin: “OR-SML: A Functional Database Programming Language for Disjunctive Information and Its Applications.” DEXA 1994: 641-650
• [IC1992] Carl A. Gunter, Elsa L. Gunter, David B. MacQueen: “Computing ML Equality Kinds Using Abstract Interpretation.” Inf. Comput. 107(2): 303-323 (1993)
• [HOL1991] Richard Gerber, Elsa L. Gunter, Insup Lee: “Implementing a Real-Time Process Algebra in HOL.” HOL 1991: 144-154
• [CADE1990] Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning: “Tutorial on Lambda-Prolog.” CADE 1990: 682
• [ELP1989] Elsa L. Gunter: “Extensions to Logic Programming Motivated by the Construction of a Generic Theorem Prover.” ELP 1989: 223-244
• [MFPS1989] Elsa L. Gunter: “Pseudo-Retract Functors for Local Lattices and Bifinite L-domains.” Mathematical Foundations of Programming Semantics 1989: 351-363
• [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

Formal Methods for Computer-Human Systems

• [ICTAC2014] Liyi Li, Elsa Gunter and William Mansky: “Symbolic Analysis Tools for CSP.” Eleventh International Colloquium on Theoretical Aspects of Computing 2014: to appear
• [ATACCS2012] Ayesha Yasmeen, Karen M. Feigh, Gabriel Gelman, Elsa L. Gunter: “Formal analysis of safety-critical system simulations.” ATACCS 2012: 71-81
• [ITP2012] William Mansky, Elsa L. Gunter: “Using Locales to Define a Rely-Guarantee Temporal Logic.” ITP 2012: 299-314
• [ISSTA2011] Ayesha Yasmeen, Elsa L. Gunter: “Automated framework for formal operator task analysis.” ISSTA 2011: 78-88
• [SMC2011a] Ayesha Yasmeen, Elsa L. Gunter: “Robustness for protection envelopes with respect to human task variation.” SMC 2011: 1809-1816
• [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
• [ECEASST2011] Ellen J. Bass, Karen M. Feigh, Elsa L. Gunter, John M. Rushby: “Formal Modeling and Analysis for Interactive Hybrid Systems.” ECEASST 45 (2011)
• [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
• [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
• [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
• [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
• [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)
• [SIGSOFT2000] Carl A. Gunter, Elsa L. Gunter, Pamela Zave: “Formal software engineering.” ACM SIGSOFT Software Engineering Notes 25(1): 54 (2000)
• [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)
• [ICRE2000] Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Pamela Zave: “A Reference Model for Requirements and Specifications-Extended Abstract.” ICRE 2000: 189
• [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

Types and Process Algebras for Security

• [NFM2013] Dennis Griffith, Elsa L. Gunter: “LiquidPi: Inferrable Dependent Session Types.” NASA Formal Methods 2013: 185-197
• [FAST2008] Elsa L. Gunter, Ayesha Yasmeen: “Secure Broadcast Ambients.” Formal Aspects in Security and Trust 2008: 257-271
• [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)
• [ENTCS2005] Eduardo Bonelli, Adriana B. Compagnoni, Elsa L. Gunter: “Typechecking Safe Process Synchronization.” Electr. Notes Theor. Comput. Sci. 138(1): 3-22 (2005)
• [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)
• [TGC2005] Adriana B. Compagnoni, Elsa L. Gunter: “Types for Security in a Mobile World.” TGC 2005: 75-97

Interactive Theorem-Proving Infrastructure (Not Mentioned Above)

• [TPHOLs1998b] Elsa L. Gunter: “Adding External Decision Procedures to HOL90 Securely.” TPHOLs 1998: 143-152
• 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 (Edited Conference Proceedings)
• 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) (Book Chapter)