| 2024 | SEFM | Verified Configuration and Deployment of Layered Attestation Managers. | Adam Petz, Will Thomas, Anna Fritz, T. J. Barclay, Logan Schmalz, Perry Alexander |
| 2024 | VECoS | Proof Repair Utilizing Large Language Models: A Case Study on the Copland Remote Attestation Proofbase. | Amer Tahat, David S. Hardin, Adam Petz, Perry Alexander |
| 2021 | MEMOCODE | Design and formal verification of a copland-based attestation protocol. | Adam Petz, Grant Jurgensen, Perry Alexander |
| 2013 | ITP | Stateless Higher-Order Logic with Quantified Types. | Evan Austin, Perry Alexander |
| 2012 | ICFP | A pattern for almost homomorphic functions. | Nicolas Frisby, Andy Gill, Perry Alexander |
| 2008 | FDL | Synthesizing Software Defined Radio Components from Rosetta (invited). | Garrin Kimmell, Ed Komp, Gary J. Minden, Joseph B. Evans, Perry Alexander |
| 2007 | GPCE | Constructing language processors with algebra combinators. | Philip Weaver, Garrin Kimmell, Nicolas Frisby, Perry Alexander |
| 2002 | RE | Multi-Faceted Requirements Modeling. | Cindy Kong, Perry Alexander |
| 2001 | EMSOFT | Heterogeneous Modeling Support for Embedded Systems Design. | Perry Alexander, Cindy Kong |
| 2000 | ICFEM | Composing Specifications in VSPEC. | Arun Venkataraman, Murali Rangarajan, Perry Alexander |
| 1999 | FM | A Brief Summary of VSPEC. | Perry Alexander, Murali Rangarajan, Phillip Baraona |
| 1996 | FM | Formal Specification and Verification of the pGVT Algorithm. | Balakrishnan Kannikeswaran, Radharamanan Radhakrishnan, Peter Frey, Perry Alexander, Philip A. Wilsey |
| 1994 | SEKE | Combining transformational and derivational analogy in Larch specification generation. | Perry Alexander |
| 1993 | SEKE | BENTON: A Multi-Agent System for Larch Specification Generation. | Perry Alexander |