| 2012 | MEMOCODE | Direct generation of invariants for reactive models. | Elizabeth I. Leonard, Myla Archer, Constance L. Heitmeyer, Ralph D. Jeffords |
| 2009 | FM | A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. | Ralph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard |
| 2007 | RE | RE Theory Meets Software Practice: Lessons from the Software Development Trenches. | Constance L. Heitmeyer, Ralph D. Jeffords, Ramesh Bharadwaj, Myla Archer |
| 2006 | CCS | Formal specification and verification of data separation in a separation kernel for an embedded system. | Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, John D. McLean |
| 2006 | MEMOCODE | Specifying and proving properties of timed I/O automata in the TIOA toolkit. | Myla Archer, Hongping Lim, Nancy A. Lynch, Sayan Mitra, Shinya Umeno |
| 2005 | MEMOCODE | Making PVS do what you want. | Myla Archer |
| 2005 | MEMOCODE | Extended abstract: organizing automaton specifications to achieve faithful representation. | Elizabeth I. Leonard, Myla Archer |
| 1999 | ACSAC | SCR: A Practical Approach to Building a High Assurance COMSEC System. | James Kirby, Myla Archer, Constance L. Heitmeyer |
| 1996 | RTAS | Mechanical verification of timed automata: a case study. | Myla Archer, Constance L. Heitmeyer |
| 1991 | RSP | Effectiveness of operating system prototyping from a template: application to MINIX. | Myla Archer, James Bock, Deborah A. Frincke, Karl N. Levitt |
| 1991 | RSP | An application of template methodology: rapid prototyping of user interface management systems. | Deborah A. Frincke, Genc L. Fisher, Myla Archer, Karl N. Levitt |
| 1990 | RSP | A template for rapid prototyping of operating systems. | Myla Archer, Deborah A. Frincke, Karl N. Levitt |