2008 |
32 | EE | 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) |
2007 |
31 | EE | 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 |
30 | EE | Myla Archer,
Thierry Boy de la Tour,
César Muñoz:
Preface.
Electr. Notes Theor. Comput. Sci. 174(11): 1-2 (2007) |
29 | EE | Hongping Lim,
Myla Archer:
Translation Templates to Support Strategy Development in PVS.
Electr. Notes Theor. Comput. Sci. 174(11): 59-79 (2007) |
2006 |
28 | EE | 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 |
27 | EE | 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 |
2005 |
26 | EE | Elizabeth I. Leonard,
Myla Archer:
Extended abstract: organizing automaton specifications to achieve faithful representation.
MEMOCODE 2005: 245-246 |
25 | EE | Myla Archer:
Making PVS do what you want.
MEMOCODE 2005: 67 |
24 | EE | Myla Archer:
Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges.
VSTTE 2005: 308-317 |
23 | | 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) |
22 | EE | Sayan Mitra,
Myla Archer:
PVS Strategies for Proving Abstraction Properties of Automata.
Electr. Notes Theor. Comput. Sci. 125(2): 45-65 (2005) |
2003 |
21 | EE | Myla Archer,
Elizabeth I. Leonard,
Matteo Pradella:
Modeling Security-Enhanced Linux Policy Specifications for Analysis.
DISCEX (2) 2003: 164-169 |
20 | EE | Myla Archer,
Elizabeth I. Leonard,
Matteo Pradella:
Analyzing Security-Enhanced Linux Policy Specifications.
POLICY 2003: 158- |
2002 |
19 | | Myla Archer,
Constance L. Heitmeyer,
Elvinia Riccobene:
Proving Invariants of I/O Automata with TAME.
Autom. Softw. Eng. 9(3): 201-232 (2002) |
2000 |
18 | EE | Myla Archer,
Constance L. Heitmeyer,
Elvinia Riccobene:
Using TAME to prove invariants of automata models: Two case studies.
FMSP 2000: 25-36 |
17 | | Myla Archer:
TAME: Using PVS strategies for special-purpose theorem proving.
Ann. Math. Artif. Intell. 29(1-4): 139-181 (2000) |
1999 |
16 | EE | James Kirby,
Myla Archer,
Constance L. Heitmeyer:
SCR: A Practical Approach to Building a High Assurance COMSEC System.
ACSAC 1999: 109-118 |
15 | EE | James Kirby Jr.,
Myla Archer,
Constance L. Heitmeyer:
Applying Formal Methods to an Information Security Device: An Experience Report.
HASE 1999: 81-88 |
14 | | Myla Archer,
Amy Lo,
Ronald A. Olsson:
Towards a Transformational Approach to Program Verification.
Softw. Test., Verif. Reliab. 9(2): 85-106 (1999) |
1998 |
13 | EE | 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) |
1997 |
12 | | Myla Archer,
Constance L. Heitmeyer:
Verifying Hybrid Systems Modeled as Timed Automata: A Case Study.
HART 1997: 171-185 |
11 | | Myla Archer,
Constance L. Heitmeyer:
Human-Style Theorem Proving Using PVS.
TPHOLs 1997: 33-48 |
1996 |
10 | EE | Myla Archer,
Constance L. Heitmeyer:
Mechanical verification of timed automata: a case study.
IEEE Real Time Technology and Applications Symposium 1996: 192-203 |
1993 |
9 | | 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 |
1992 |
8 | | Myla Archer,
Jeffrey J. Joyce,
Karl N. Levitt,
Phillip J. Windley:
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA
IEEE Computer Society 1992 |
7 | | 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 |
6 | | Saraswati Kalvala,
Myla Archer,
Karl N. Levitt:
Implementation and Use of Annotations in HOL.
TPHOLs 1992: 407-426 |
5 | | 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 |
4 | | Myla Archer,
George Fink,
Lie Yang:
Linking Other Theorem Provers to HOL Using PM: Proof Manager.
TPHOLs 1992: 539-548 |
1991 |
3 | | Deborah A. Frincke,
Myla Archer,
Karl N. Levitt:
CTPLAN: A Planning-Based Approach to Automatically Detecting Flaws in Concurrent Algorithms.
KBSE 1991: 151-160 |
2 | | George Fink,
Myla Archer,
Lie Yang:
PM: A Proof Manager for HOL and Other Provers.
TPHOLs 1991: 286-304 |
1984 |
1 | | Samuel N. Kamin,
Myla Archer:
Partial Implementations of Abstract Data Types: A Dissenting view on Errors.
Semantics of Data Types 1984: 317-336 |