Myla Archer

Myla Archer, Elizabeth I. Leonard, Constance L. Heitmeyer: Idea: Writing Secure C Programs with SecProve. ESSoS 2013: 171-180

Elizabeth I. Leonard, Myla Archer, Constance L. Heitmeyer, Ralph D. Jeffords: Direct generation of invariants for reactive models. MEMOCODE 2012: 119-130

Ralph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard: Model-based construction and verification of critical systems using composition and partial refinement. Formal Methods in System Design 37(2-3): 265-294 (2010)

Ralph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard: A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. FM 2009: 173-189

Myla Archer, Hongping Lim, Nancy A. Lynch, Sayan Mitra, Shinya Umeno: Specifying and proving properties of timed I/O automata using Tempo. Design Autom. for Emb. Sys. 12(1-2): 139-170 (2008)

Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, John McLean: Applying Formal Methods to a Certifiably Secure Software System. IEEE Trans. Software Eng. 34(1): 82-98 (2008)

Myla Archer, Thierry Boy de la Tour, César Muñoz: Preface. Electr. Notes Theor. Comput. Sci. 174(11): 1-2 (2007)

Hongping Lim, Myla Archer: Translation Templates to Support Strategy Development in PVS. Electr. Notes Theor. Comput. Sci. 174(11): 59-79 (2007)

Constance L. Heitmeyer, Ralph D. Jeffords, Ramesh Bharadwaj, Myla Archer: RE Theory Meets Software Practice: Lessons from the Software Development Trenches. RE 2007: 265-268

Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, John D. McLean: Formal specification and verification of data separation in a separation kernel for an embedded system. ACM Conference on Computer and Communications Security 2006: 346-355

Myla Archer, Hongping Lim, Nancy A. Lynch, Sayan Mitra, Shinya Umeno: Specifying and proving properties of timed I/O automata in the TIOA toolkit. MEMOCODE 2006: 129-138

Constance L. Heitmeyer, Myla Archer, Ramesh Bharadwaj, Ralph D. Jeffords: Tools for constructing requirements specifications: the SCR Toolset at the age of nine. Comput. Syst. Sci. Eng. 20(1) (2005)

Sayan Mitra, Myla Archer: PVS Strategies for Proving Abstraction Properties of Automata. Electr. Notes Theor. Comput. Sci. 125(2): 45-65 (2005)

Myla Archer: Making PVS do what you want. MEMOCODE 2005: 67

Elizabeth I. Leonard, Myla Archer: Extended abstract: organizing automaton specifications to achieve faithful representation. MEMOCODE 2005: 245-246

Myla Archer: Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges. VSTTE 2005: 308-317

Myla Archer, Elizabeth I. Leonard, Matteo Pradella: Modeling Security-Enhanced Linux Policy Specifications for Analysis. DISCEX (2) 2003: 164-169

Myla Archer, Elizabeth I. Leonard, Matteo Pradella: Analyzing Security-Enhanced Linux Policy Specifications. POLICY 2003: 158-

Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene: Proving Invariants of I/O Automata with TAME. Autom. Softw. Eng. 9(3): 201-232 (2002)

Myla Archer: TAME: Using PVS strategies for special-purpose theorem proving. Ann. Math. Artif. Intell. 29(1-4): 139-181 (2000)

Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene: Using TAME to prove invariants of automata models: Two case studies. FMSP 2000: 25-36

Myla Archer, Amy Lo, Ronald A. Olsson: Towards a Transformational Approach to Program Verification. Softw. Test., Verif. Reliab. 9(2): 85-106 (1999)

James Kirby, Myla Archer, Constance L. Heitmeyer: SCR: A Practical Approach to Building a High Assurance COMSEC System. ACSAC 1999: 109-118

James Kirby Jr., Myla Archer, Constance L. Heitmeyer: Applying Formal Methods to an Information Security Device: An Experience Report. HASE 1999: 81-88

Constance L. Heitmeyer, James Kirby, Bruce G. Labaw, Myla Archer, Ramesh Bharadwaj: Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications. IEEE Trans. Software Eng. 24(11): 927-948 (1998)

Myla Archer, Constance L. Heitmeyer: Verifying Hybrid Systems Modeled as Timed Automata: A Case Study. HART 1997: 171-185

Myla Archer, Constance L. Heitmeyer: Human-Style Theorem Proving Using PVS. TPHOLs 1997: 33-48

Myla Archer, Constance L. Heitmeyer: Mechanical verification of timed automata: a case study. IEEE Real Time Technology and Applications Symposium 1996: 192-203

Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark Heckman, Gregory D. Benson: Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL. HUG 1993: 29-42

William L. Harrison, Myla Archer, Karl N. Levitt: A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language. TPHOLs 1992: 347-356

Saraswati Kalvala, Myla Archer, Karl N. Levitt: Implementation and Use of Annotations in HOL. TPHOLs 1992: 407-426

Jing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala: Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit. TPHOLs 1992: 427-447

Myla Archer, George Fink, Lie Yang: Linking Other Theorem Provers to HOL Using PM: Proof Manager. TPHOLs 1992: 539-548

Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (Eds.): Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA. IEEE Computer Society 1992

Deborah A. Frincke, Myla Archer, Karl N. Levitt: CTPLAN: A Planning-Based Approach to Automatically Detecting Flaws in Concurrent Algorithms. KBSE 1991: 151-160

George Fink, Myla Archer, Lie Yang: PM: A Proof Manager for HOL and Other Provers. TPHOLs 1991: 286-304

Samuel N. Kamin, Myla Archer: Partial Implementations of Abstract Data Types: A Dissenting view on Errors. Semantics of Data Types 1984: 317-336