Found 181 results
Moskowitz, I. S., G. E. Longdon, and LW. Chang, "A New Paradigm Hidden in Steganography", New Security Paradigms Workshop, Cork, Ireland, Ballycotton, Co., 2000. PDF icon Moskowitz etal2000.pdf (247.73 KB)
Syverson, P., M. Reed, and D. Goldschlag, "Onion Routing Access Configurations", DISCEX 2000: Proceedings of the DARPA Information Survivability Conference and Exposition, vol. 1, Hilton Head, South Carolina, IEEE Computer Society Press, pp. 34-40, 2000. PDF icon Syverson etal2000c.pdf (154.68 KB)
Meadows, C., "Open Issues in Formal Methods for Cryptographic Protocol Analysis", DISCEX 2000: IEEE Computer Society Press, pp. 237-250, 2000. PDF icon Meadows2000d.pdf (168.94 KB)
Bharadwaj, R., and S. Sims, "Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking", Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000): Springer, 2000. PDF icon BharadwajSims2000.pdf (265.25 KB)
Archer, M., "TAME: Using PVS Strategies for Special-Purpose Theorem Proving", Annals of Mathematics and Artificial Intelligence, vol. 29, issue 1-4, pp. 139-181, 2000. PDF icon Archer2000.pdf (462.98 KB)
Syverson, P., G. Tsudik, M. Reed, and C. Landwehr, "Towards an Analysis of Onion Routing Security", Workshop on Design Issues in Anonymity and Unobservability, Berkeley, California, 2000. PDF icon Syverson etal2000b.pdf (252.37 KB)
"Using TAME to Prove Invariants of Automata Models: Two Case Studies", Third ACM Workshop on Formal Methods in Software Practice (FMSP'00), Portland, Oregon, pp. 25-36, 2000.
Bharadwaj, R., and C. L. Heitmeyer, "Model Checking Complete Requirements Specifications Using Abstraction", Automated Software Engineering, vol. 6, issue 1, pp. 37-68, 1999. PDF icon BharadwajHeitmeyer1999.pdf (171.03 KB)
"SCR: A Practical Approach to Building a High Assurance COMSEC System", 15th Annual Computer Security Applications Conference (ACSAC '99): IEEE Computer Society Press, 1999.
Gargantini, A., and C. L. Heitmeyer, "Using Model Checking to Generate Tests from Requirements Specifications", Joint 7th Eur. Software Engineering Conf. and 7th ACM SIGSOFT Intern. Symp. on Foundations of Software Eng. (ESEC/FSE99), Toulouse, France, 1999. PDF icon GargantiniHeitmeyer1999.pdf (261.95 KB)
Jeffords, R., and C. L. Heitmeyer, "Automatic Generation of State Invariants from Requirements Specifications", 6th International Symposium on the Foundations of Software Engineering (FSE-6), Orlando, Florida, 1998. PDF icon JeffordsHeitmeyer1998.pdf (344.8 KB)
Archer, M., and C. L. Heitmeyer, "Mechanical Verification of Timed Automata: A Case Study", NRL Memorandum Report, no. 5546-98-8180, 1998. PDF icon ArcherHeitmeyer1998.pdf (678.22 KB)
Heitmeyer, C. L., "On the Need for 'Practical' Formal Methods", Formal Techniques in Real-Time and Real-Time Fault-Tolerant Systems, 5th Intern. Symposium (FTRTFT'98), vol. LICS 1486, Lyngby, Denmark, pp. 18-26, 1998. PDF icon Heitmeyer1998.pdf (138.88 KB)
Heitmeyer, C. L., J. Kirby, Jr, B. Labaw, and R. Bharadwaj, "SCR*: A Toolset for Specifying and Analyzing Software Requirements", Computer-Aided Verification, 10th Ann. Conf. (CAV'98), Vancouver, BC, Canada, 1998. PDF icon Heitmeyer etal1998.pdf (154.77 KB)
Archer, M., C. L. Heitmeyer, and S. Sims, "TAME: A PVS Interface to Simplify Proofs for Automata Models", UITP, 1998. PDF icon Archer etal1998.pdf (199.67 KB)
Heitmeyer, C. L., J. Kirby, Jr, B. Labaw, M. Archer, and R. Bharadwaj, "Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications", IEEE Transactions on Software Engineering, vol. 24, issue 11, 1998. PDF icon Heitmeyer etal1998b.pdf (897.72 KB)
Bharadwaj, R., and C. L. Heitmeyer, "Applying the SCR Requirements Method to a Simple Autopilot", Fourth NASA Langley Formal Methods Workshop, Hampton, Virginia, 1997. PDF icon BharadwajHeitmeyer1997b.pdf (289.85 KB)
Archer, M., and C. L. Heitmeyer, "Human-Style Theorem Proving Using PVS", TPHOLs, Murray Hill, New Jersey, 1997. PDF icon ArcherHeitmeyer1997.pdf (220.72 KB)
Archer, M., and C. L. Heitmeyer, "Verifying Hybrid Systems Modeled as Timed Automata: A Case Study", HART, Grenoble, France, 1997. PDF icon ArcherHeitmeyer1997b.pdf (178.46 KB)
Bharadwaj, R., and C. L. Heitmeyer, "Verifying SCR Requirements Specifications using State Exploration", First ACM SIGPLAN Workshop on Automatic Analysis of Software, Paris, France, 1997. PDF icon BharadwajHeitmeyer1997.pdf (248.61 KB)
Heitmeyer, C. L., R. Jeffords, and B. Labaw, "Automated Consistency Checking of Requirements Specifications", ACM Transactions on Software Engineering and Methodology, vol. 5, issue 3, pp. 231-261, 1996. PDF icon Heitmeyer etal1996.pdf (394.91 KB)
Archer, M., and C. L. Heitmeyer, "Mechanical Verification of Timed Automata: A Case Study", 996 Real-Time Technology and Applications Symposium, 1996. PDF icon ArcherHeitmeyer1996.pdf (232.16 KB)
Archer, M., and C. L. Heitmeyer, "TAME: A Specialized Specification and Verification System for Timed Automata", Work in Progress session at RTSS, Washington, D.C., 1996. PDF icon ArcherHeitmeyer1996b.pdf (134.07 KB)
Heitmeyer, C. L., and B. Labaw, "Consistency Checking of SCR-Style Requirements Specifications", International Symposium on Requirements Engineering, York, England, 1995. PDF icon HeitmeyerLabaw1995.pdf (257.28 KB)
McLean, J., and C. L. Heitmeyer, "High Assurance Computer Systems: A Research Agenda", America in the Age of Information, National Science and Technology Council Committee on Information and Communications Forum, Bethesda, Maryland, 1995. PDF icon McLeanHeitmeyer1995.pdf (103.99 KB)