Found 24 results
Filters: Author is Archer, Myla [Clear All Filters]
"A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition", Formal Methods, Second World Congress (FM 2009), Eindhoven, The Netherlands, pp. 173-189, 2009.
"RE Theory Meets Software Practice: Lessons from the Software Development Trenches", 15th IEEE International Requirements Engineering Conference, New Delhi, India, pp. 265-268, 2007.
"Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode", Proceedings of VERIFY'06, The Third International Verification Workshop, Seattle, Washington, 2006.
"Formal specification and verification of data separation in a separation kernel for an embedded system", 13th ACM Conference on Computer and Communications Security (CCS 2006), Alexandria, Virginia, pp. 346-355, 2006.
"Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit", Fourth ACM \& IEEE International Conference on Formal Methods and Models for Co-Design, Napa, California, pp. 129-138, 2006.
"Translation Templates to Support Strategy Development in PVS", STRATEGIES06, The Sixth International Workshop on Strategies in Automated Deduction, Seattle, Washington, 2006.
"Extended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation", Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05), Verona, Italy, 2005.
"PVS Proof Strategies for Proving Abstraction Properties of Automata", Electronic Notes in Theoretical Computer Science, vol. 125, pp. 45-65, 2005.
"Tools for constructing requirements specifications: The SCR toolset at the age of ten", International Journal of Computer Systems Science and Engineering, vol. 20, issue 1, pp. 19-35, 2005.
"Basing a Modeling Environment on a General Purpose Theorem Prover", 2004 Monterey Workshop on Software Engineering Tools: Compatibility and Integration, Baden, Austria, 2004.
"Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata", Fourth International Workshop on Strategies in Automated Deduction (STRATEGIES 2004), Cork, Ireland, 2004.
"Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata", First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), Rome, Italy, 2003.
"Modeling Security-Enchanced Linux Policy Specifications for Analysis", Research Summaries for DISCEX III, Washington, D.C., 2003.
"Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME", WITS '02, Portland, Oregon, 2002.
"Proving Invariants of I/O Automata with TAME", Automated Software Engineering, vol. 9, pp. 201-232, 2002.
"Applying TAME to I/O Automata: A User's Perspective", NRL Memorandum Report, no. 5540-00-8848, 2000.
"TAME: Using PVS Strategies for Special-Purpose Theorem Proving", Annals of Mathematics and Artificial Intelligence, vol. 29, issue 1-4, pp. 139-181, 2000.
"Mechanical Verification of Timed Automata: A Case Study", NRL Memorandum Report, no. 5546-98-8180, 1998.
"TAME: A PVS Interface to Simplify Proofs for Automata Models", UITP, 1998.
"Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications", IEEE Transactions on Software Engineering, vol. 24, issue 11, 1998.
"Human-Style Theorem Proving Using PVS", TPHOLs, Murray Hill, New Jersey, 1997.
"Verifying Hybrid Systems Modeled as Timed Automata: A Case Study", HART, Grenoble, France, 1997.
"Mechanical Verification of Timed Automata: A Case Study", 996 Real-Time Technology and Applications Symposium, 1996.
"TAME: A Specialized Specification and Verification System for Timed Automata", Work in Progress session at RTSS, Washington, D.C., 1996.