Students of
Elsa L Gunter
Current PhD Students
Dennis Griffith, UIUC
Papers from work at UIUC
Robustness for protection envelopes with respect to human task variation
(GRAPHITE 2014)
LiquidPi: Inferrable Dependent Session Types
Toward a multi-method approach to formalizing human-automation interaction and human-human communications
(SMC 2011)
Below were supervised by Prof. Grigore Rosu
An overview of the MOP runtime verification framework
(STTT 2012)
Garbage collection for monitoring parametric properties
(PLDI 2011)
Susannah Johnson, UIUC
Area of Interest
Applications a formal methods to security
Liyi Li, UIUC
Papers from work at UIUC
Symbolic Analysis Tools for CSP
(ICTAC 2014)
Graduated PhD Students
William Mansky, UIUC, May 2014
Publications from work at UIUC
A Cross-Language Framework for Verifying Compiler Optimizations
(LOLA 2014)
Verifying Optimizations for Concurrent Programs
(WPTE 2014)
Robustness for protection envelopes with respect to human task variation
(GRAPHITE 2014)
Symbolic Analysis Tools for CSP
(ICTAC 2014)
Using Locales to Define a Rely-Guarantee Temporal Logic
(ITP 2012)
Toward a multi-method approach to formalizing human-automation interaction and human-human communications
(SMC 2011)
A Framework for Formal Verification of Compiler Optimizations
(ITP 2010)
Thesis
Specifying and Verifying Program Transformations with PTRANS
Ayesha Yasmeen, UIUC, June 2011
Publications from work at UIUC
Formal analysis of safety-critical system simulations
(ATACCS 2012)
Automated framework for formal operator task analysis
(ISSTA 2011)
Robustness for protection envelopes with respect to human task variation
(SMC 2011)
Specifying and Analyzing Workflows for Automated Identification and Data Capture
(HICSS 2009)
Secure Broadcast Ambients
(FAST 2008)
Thesis
Formalizing Operator Task Analysis
Andrei Popescu
, UIUC, Oct 2010
Publications from work at UIUC
Recursion principles for syntax with bindings and substitution
(ICFP 2011)
Strong Normalization for System F by HOAS on Top of FOAS
(LICS 2010)
Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
(FOSSACS 2010)
Theory support for weak higher order abstract syntax in Isabelle/HOL
(LFMTP 2009)
Ordinals and Cardinals
(AFP 2009)
Below were supervised by Prof. Grigore Rosu
A Semantic Approach to Interpolation
(TCS 410(12-13): 1109-1128 (2009))
Term-Generic Logic
(WADT 2008)
An Institution-Independent Proof of the Robinson Consistency Theorem
(Studia Logica 85(1): 41-73 (2007))
An Institution-independent Generalization of Tarski's Elementary Chain Theorem
(JLC 16(6): 713-735 (2006))
Behavioral Extensions of Institutions
(CALCO 2005)
Weak bisimilarity coalgebraically
(CALCO 2009)
Languages Generated Using an Abstract Catenation
(Grammars 7, 2004)
Thesis
Contributions to the Theory of Syntax with Bindings and to Process Algebra
Yi Meng, NJIT, May 2006
Thesis
An Automata-Based Automatic Verification Environment
