Rob Lorch --------- PhD Candidate, Computer Science @ UIowa Research Interests: - Automated reasoning - Computer security Email: robert-lorch@uiowa.edu Links: Google Scholar CV GitHub About ----- I'm a fourth-year computer science PhD candidate at the University of Iowa, where I am a member of the Computational Logic Center. I work under the supervision of Dr. Cesare Tinelli and Dr. Omar Chowdhury (@ Stony Brook University). Broadly speaking, I am interested in automated techniques for detecting security vulnerabilities in computational systems, or proving their absence. In my work, I employ and develop tools and techniques from the field of automated reasoning (including SMT solvers, model checkers, deductive verification engines, and so on). Publications ------------ ICSE '26. R. Lorch, D. Dar, C. Tinelli, and O. Chowdhury, "Parse this! Summoning Context-Sensitive Inputs with Goblin" [pdf] ^ In this paper, I develop a new approach for context-sensitive input generation (i.e., given a context-sensitive grammar G, find x such that x \in G) utilizing SMT solvers. Such an input generation tool can be used to fuzz software with complex inputs (e.g. pdf parsers), as one can encode the input specification as a context-sensitive grammar. We applied this approach in [S&P '25] (see below) to discover security vulnerabilities in a widely-used implementation of the Wi-Fi SAE handshake protocol. Systems Engineering '26. B. Meng, R. Lorch, K. Siu, M. Durling, S. Varanasi, S. Paul, and A. Moitra, "Transforming Natural Language Requirements to Formalism Using LLMs" [pdf] S&P '25. D. Dar, R. Lorch, A. Sadeghi, V. Sorcigli, H. Gollier, C. Tinelli, M. Vanhoef, and O. Chowdhury, "SAECRED: A State-Aware, Over-the-Air Protocol Testing Approach for Discovering Parsing Bugs in SAE Handshake Implementations of COTS Wi-Fi Access Points" [pdf] NFM '25. B. Meng, S. Varanasi, R. Lorch, A. Moitra, K. Siu, S. Paul, M. Durling, N. Beniwal and N. Visnevski, "TRACE: Toolkit for Requirements Analysis Capture and Elicitation" [pdf] RAID '24. R. Lorch, D. Larraz, C. Tinelli, and O. Chowdhury, "A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework" [pdf] ^ In this paper, I explore novel techniques for interoperation between cryptographic protocol verifiers (e.g., Tamarin) and general-purpose model checkers (e.g., Kind 2) aimed towards the discovery of design-level vulnerabilities in security protocols. FormaliSE '24. R. Lorch, B. Meng, K. Siu, A. Moitra, M. Durling, S. Paul, S. Varanasi, and C. McMillan, "Formal Methods in Requirements Engineering: Survey and Future Directions" [pdf] FMCAD '23. D. Larraz, R. Lorch, M. Yahyazadeh, F. Arif, O. Chowdhury, and C. Tinelli, "CRV: Automated Cyber-Resiliency Reasoning for System Design Models" [pdf] Australasian Journal of Combinatorics '22. B. Carrigan, D. Diaz, J. Hammer, J. Lorch, and R. Lorch, "Constructing (3, b)-sudoku pair Latin squares" [pdf] Bulletin of the Institute of Combinatorics and its Applications '21. B. Carrigan, J. Hammer, J. Lorch, R. Lorch, and C. Owens, "List colorings count rokudoku-pair squares" [pdf] Teaching -------- Below is a list of courses I have taught in various capacities. * UIowa Teaching Assistant [CS:4420, Spring '22] Artificial Intelligence [CS:5810, Fall '21] Formal Methods in Software Engineering [CS:2640, Fall '21] Computer Organization * Grinnell College Class Mentor [CSC-207, Spring '21] Object-oriented data structures and algorithms * Grinnell College Peer Tutor [CSC-161, Spring '21] Imperative problem solving and data structures