Code 5546 is the Software Engineering Section in the Center for High Assurance Computer Systems Branch of the Information Technology Division.

The section's mission is to conduct research in and to develop technology for high assurance software. The primary thrust of the research is the formulation of mathematically based methods, models, algorithms, and theories supporting both the construction as well as the analysis of software at different levels of abstraction from requirements through binary code. Researchers in the section work closely with developers and evaluators of Naval and other government systems to transfer the results of the section's research to software practice.

Model-Based Software Development and Analysis
  • Requirements Specification, Validation and Verification
  • Compositional Software Construction and Verification
  • Assertion-Based Analysis of Software Models
  • Hardware/Software Co-Design
  • Fault-Tolerant Computing
  • Real-Time Computing

Selected Publications

2009 Heitmeyer CL.  2009.  On the Role of Formal Methods in Software Certification: An Experience Report. Electronic Notes in Theoretical Computer Science . 238(4):3-9.PDF icon Heitmeyer2009.pdf (189.1 KB)
2009 Jeffords R, Heitmeyer CL, Archer M, Leonard E.  2009.  A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. Formal Methods, Second World Congress (FM 2009). :173-189.PDF icon Jeffords etal2009.pdf (144.97 KB)
2008 [Anonymous].  2008.  Applying Formal Methods to a Certifiably Secure Software System. IEEE Transactions on Software Engineering. 34(1):82-98.
2008 [Anonymous].  2008.  Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems. Design Automation for Embedded Systems. 12(1-2):97-137.
2007 Heitmeyer CL, Jeffords R, Bharadwaj R, Archer M.  2007.  RE Theory Meets Software Practice: Lessons from the Software Development Trenches. 15th IEEE International Requirements Engineering Conference. :265-268.PDF icon Heitmeyer etal2007.pdf (521.34 KB)
2007 Heitmeyer CL.  2007.  Formal Methods for Specifying, Validating, and Verifying Requirements. Journal of Computer Science. 13(5):607-618.PDF icon Heitmeyer2007.pdf (466.65 KB)
2007 Heitmeyer CL, Jeffords R.  2007.  Applying a Formal Requirements Method to Three NASA Systems: Lessons Learned. 2007 IEEE Aerospace Conference. PDF icon HeitmeyerJeffords2007.pdf (616.1 KB)
2006 Archer M, Leonard E.  2006.  Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode. Proceedings of VERIFY'06, The Third International Verification Workshop. PDF icon ArcherLeonard2006.pdf (2.14 MB)
2006 Bultan T, Heitmeyer CL.  2006.  Analyzing Tabular Requirements Specifications Using Infinite State Model Checking. Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06). PDF icon BultanHeitmeyer2006.pdf (163.42 KB)
2006 Heitmeyer CL, Archer M, Leonard E, McLean J.  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). :346-355.PDF icon Heitmeyer etal2006.pdf (265.8 KB)
2006 Rothamel T, Liu YA, Heitmeyer CL, Leonard E.  2006.  Generating Optimized Code from SCR Specifications. ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006). PDF icon Rothamel etal2006.pdf (159.88 KB)
2006 Lim HP, Archer M.  2006.  Translation Templates to Support Strategy Development in PVS. STRATEGIES06, The Sixth International Workshop on Strategies in Automated Deduction. PDF icon LimArcher2006.pdf (2.52 MB)
2005 Heitmeyer CL, Archer M, Bharadwaj R, Jeffords R.  2005.  Tools for constructing requirements specifications: The SCR toolset at the age of ten. International Journal of Computer Systems Science and Engineering. 20(1):19-35.PDF icon Heitmeyer etal2005.pdf (774.15 KB)
2005 Leonard E, Archer M.  2005.  Extended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation. Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05). PDF icon LeonardArcher2005.pdf (88.94 KB)
2005 Luo J, Montrose B, Kang M.  2005.  An Approach for Semantic Query Processing with UDDI. Agents, Web Services and Ontologies Merging. PDF icon Luo etal2005.pdf (240.06 KB)
2005 Mitra S, Archer M.  2005.  PVS Proof Strategies for Proving Abstraction Properties of Automata. Electronic Notes in Theoretical Computer Science. 125:45-65.PDF icon MitraArcher2005.pdf (486.64 KB)
2005 [Anonymous].  2005.  Point/Counterpoint. IEEE Software. 22(1):48-51.
2005 Jeffords R, Bharadwaj R.  2005.  Extended Abstract: Formal Verification of Architectural Patterns in Support of Dependable Distributed Systems. Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05). PDF icon JeffordsBharadwaj2005.pdf (59.54 KB)
2004 Jeffords R, Leonard E.  2004.  Using Invariants to Optimize Formal Specifications Before Code Synthesis. 2nd ACM/IEEE Int'l Conf. on Formal Methods and Models for Co-Design (MEMOCODE 2004). PDF icon JeffordsLeonard2004.pdf (127.34 KB)
2004 Heitmeyer CL.  2004.  Managing complexity in software development with formally based tools. ETAPS Workshop on Formal Foundations of Software and Component-Based Software Architectures (FESCA 2004). PDF icon Heitmeyer2004.pdf (175.67 KB)
2004 Mitra S, Archer M.  2004.  Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata. Fourth International Workshop on Strategies in Automated Deduction (STRATEGIES 2004). PDF icon MitraArcher2004.pdf (486.64 KB)
2004 Archer M.  2004.  Basing a Modeling Environment on a General Purpose Theorem Prover. 2004 Monterey Workshop on Software Engineering Tools: Compatibility and Integration. PDF icon Archer2004.pdf (10.51 MB)
2003 [Anonymous].  2003.  Developing User Strategies in PVS: A Tutorial. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003).
2003 Archer M, Leonard E, Pradella M.  2003.  Modeling Security-Enchanced Linux Policy Specifications for Analysis. Research Summaries for DISCEX III. PDF icon Archer etal2003.pdf (192.2 KB)
2003 [Anonymous].  2003.  Analyzing Security-Enhanced Linux Policy Specifications. IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY 2003).
2003 Bharadwaj R.  2003.  Secure Middleware for Situation-Aware Naval C2 and Combat Systems. 9th International Workshop on Future Trends of Distributed Comput ing Systems (FTDCS 2003). PDF icon Bharadwaj2003.pdf (169.53 KB)
2003 Bharadwaj R.  2003.  How to Fake a Rational Design Process using the SCR Method. Software Engineering for High Assurance Systems (SEHAS 2003). PDF icon Bharadwaj2003b.pdf (75.62 KB)
2003 Bharadwaj R.  2003.  A Framework for the Formal Analysis of Multi-Agent Systems. Formal Approaches to Multi-Agent Systems (FAMAS), affiliated with ETAPS 2003. PDF icon Bharadwaj2003c.pdf (228.44 KB)
2003 Jeffords R, Heitmeyer CL.  2003.  A Strategy for Efficiently Verifying Requirements Specifications Using Composition and Invariants. European Software Engineering Conference/ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003). PDF icon JeffordsHeitmeyer2003.pdf (211.53 KB)
2003 Kim SE, In P, Bharadwaj R.  2003.  An Extended Framework for the Validation and Verification of Situation-Aware Middleware Architectures. Proceedings Ground System Architectures Workshop (GSAW 2003). PDF icon Kim etal2003.pdf (52.47 KB)
2003 Leonard E, Heitmeyer CL.  2003.  Program Synthesis from Formal Requirements Specifications using APTS. Higher-Order and Symbolic Computation. 16(1-2):63-92.PDF icon LeonardHeitmeyer2003.pdf (164.15 KB)
2003 Mitra S, Archer M.  2003.  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). PDF icon MitraArcher2003.pdf (159.7 KB)
2003 Bharadwaj R.  2003.  Verifiable Middleware for Secure Agent Interoperability. 2nd Goddard IEEE Workshop on Formal Approaches to Agent-Based Systems. PDF icon Bharadwaj2003d.pdf (183.81 KB)
2003 [Anonymous].  2003.  Analyzing Security-Enhanced Linux Policy Specifications. NRL Memorandum Report.
2002 Archer M, Heitmeyer CL, Riccobene E.  2002.  Proving Invariants of I/O Automata with TAME. Automated Software Engineering. 9:201-232.PDF icon Archer etal2002.pdf (355.28 KB)
2002 Archer M.  2002.  Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME. WITS '02. PDF icon Archer2002.pdf (191.65 KB)
2002 Bharadwaj R.  2002.  Formal Analysis of Domain Models. International Workshop on Requirements for High Assurance Systems (RHAS'02). PDF icon Bharadwaj2002.pdf (200.72 KB)
2002 Bharadwaj R.  2002.  SINS: A middleware for autonomous agents and secure code mobility. Second International Workshop on Security of Mobile Multi-Agent Systems (SEMAS-02), First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002). PDF icon Bharadwaj2002b.pdf (119.17 KB)
2002 Bharadwaj R.  2002.  SOL: A Verifiable Synchronous Language for Reactive Systems. Synchronous Languages, Applications, and Programming (SLAP'02), ETAPS'2002. PDF icon Bharadwaj2002c.pdf (219.78 KB)
2002 Bharadwaj R, Froscher J, Khashnobish A, Tracy J.  2002.  An Infrastructure for Secure Interoperability of Agents. Sixth World Multiconference on Systemics, Cybernetics, and Informatics. PDF icon Bharadwaj etal2002.pdf (32.11 KB)
2002 [Anonymous].  2002.  Verifiable Middleware for Secure Agent Interoperability. Second Goddard IEEE Workshop on Formal Approaches to Agent-Based Systems (FAABS II).
2002 Heitmeyer CL, Marciniak JJ.  2002.  Software Cost Reduction. Encyclopedia of Software Engineering. 2PDF icon Heitmeyer2002.pdf (220.45 KB)
2002 Kirby, Jr J.  2002.  Rewriting Requirements for Design. IASTED International Conference on Software Engineering and Applications (SEA) 2002. PDF icon Kirby2002.pdf (274.15 KB)
2002 [Anonymous].  2002.  Towards a Methodology and Tool for the Analysis of Security-Enhanced Linux Security Policies. NRL Memorandum Report.
2001 Heitmeyer CL.  2001.  Applying 'Practical' Formal Methods to the Specification and Analysis of Security Properties. Information Assurance in Computer Networks (MMM-ACNS 2001). PDF icon Heitmeyer2001.pdf (137.38 KB)
2001 Jeffords R, Heitmeyer CL.  2001.  An Algorithm for Strengthening State Invariants Generated from Requirements Specifications. Fifth IEEE Int'l Symp. on Requirements Engineering (RE'01). PDF icon JeffordsHeitmeyer2001.pdf (344.59 KB)
2000 Riccobene E, Archer M, Heitmeyer CL.  2000.  Applying TAME to I/O Automata: A User's Perspective. NRL Memorandum Report. PDF icon Riccobene etal2000.pdf (318 KB)
2000 Archer M.  2000.  TAME: Using PVS Strategies for Special-Purpose Theorem Proving. Annals of Mathematics and Artificial Intelligence. 29(1-4):139-181.PDF icon Archer2000.pdf (462.98 KB)
2000 [Anonymous].  2000.  Using TAME to Prove Invariants of Automata Models: Two Case Studies. Third ACM Workshop on Formal Methods in Software Practice (FMSP'00). :25-36.
2000 Bharadwaj R, Heitmeyer CL.  2000.  Developing High Assurance Avionics Systems with the SCR Requirements Method. 19th Digital Avionics Systems Conference. PDF icon BharadwajHeitmeyer2000.pdf (71.48 KB)
2000 Bharadwaj R, Sims S.  2000.  Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000). PDF icon BharadwajSims2000.pdf (265.25 KB)
2000 Heitmeyer CL, Bharadwaj R.  2000.  Applying the SCR Requirements Method to the Light Control Case Study. Journal of Universal Computer Science. PDF icon HeitmeyerBharadwaj2000.pdf (363.13 KB)
1999 Bharadwaj R, Heitmeyer CL.  1999.  Model Checking Complete Requirements Specifications Using Abstraction. Automated Software Engineering. 6(1):37-68.PDF icon BharadwajHeitmeyer1999.pdf (171.03 KB)
1999 Gargantini A, Heitmeyer CL.  1999.  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). PDF icon GargantiniHeitmeyer1999.pdf (261.95 KB)
1999 [Anonymous].  1999.  SCR: A Practical Approach to Building a High Assurance COMSEC System. 15th Annual Computer Security Applications Conference (ACSAC '99).
1998 Heitmeyer CL.  1998.  On the Need for 'Practical' Formal Methods. Formal Techniques in Real-Time and Real-Time Fault-Tolerant Systems, 5th Intern. Symposium (FTRTFT'98). LICS 1486:18-26.PDF icon Heitmeyer1998.pdf (138.88 KB)
1998 Heitmeyer CL, Kirby, Jr J, Labaw B, Bharadwaj R.  1998.  SCR*: A Toolset for Specifying and Analyzing Software Requirements. Computer-Aided Verification, 10th Ann. Conf. (CAV'98). PDF icon Heitmeyer etal1998.pdf (154.77 KB)
1998 Heitmeyer CL, Kirby, Jr J, Labaw B, Archer M, Bharadwaj R.  1998.  Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications. IEEE Transactions on Software Engineering. 24(11)PDF icon Heitmeyer etal1998b.pdf (897.72 KB)
1998 Jeffords R, Heitmeyer CL.  1998.  Automatic Generation of State Invariants from Requirements Specifications. 6th International Symposium on the Foundations of Software Engineering (FSE-6). PDF icon JeffordsHeitmeyer1998.pdf (344.8 KB)
1998 Archer M, Heitmeyer CL, Sims S.  1998.  TAME: A PVS Interface to Simplify Proofs for Automata Models. UITP. PDF icon Archer etal1998.pdf (199.67 KB)
1998 Archer M, Heitmeyer CL.  1998.  Mechanical Verification of Timed Automata: A Case Study. NRL Memorandum Report. PDF icon ArcherHeitmeyer1998.pdf (678.22 KB)
1997 Archer M, Heitmeyer CL.  1997.  Human-Style Theorem Proving Using PVS. TPHOLs. PDF icon ArcherHeitmeyer1997.pdf (220.72 KB)
1997 Archer M, Heitmeyer CL.  1997.  Verifying Hybrid Systems Modeled as Timed Automata: A Case Study. HART. PDF icon ArcherHeitmeyer1997b.pdf (178.46 KB)
1997 Bharadwaj R, Heitmeyer CL.  1997.  Verifying SCR Requirements Specifications using State Exploration. First ACM SIGPLAN Workshop on Automatic Analysis of Software. PDF icon BharadwajHeitmeyer1997.pdf (248.61 KB)
1997 Bharadwaj R, Heitmeyer CL.  1997.  Applying the SCR Requirements Method to a Simple Autopilot. Fourth NASA Langley Formal Methods Workshop. PDF icon BharadwajHeitmeyer1997b.pdf (289.85 KB)
1996 Heitmeyer CL, Jeffords R, Labaw B.  1996.  Automated Consistency Checking of Requirements Specifications. ACM Transactions on Software Engineering and Methodology. 5(3):231-261.PDF icon Heitmeyer etal1996.pdf (394.91 KB)
1996 Archer M, Heitmeyer CL.  1996.  Mechanical Verification of Timed Automata: A Case Study. 996 Real-Time Technology and Applications Symposium. PDF icon ArcherHeitmeyer1996.pdf (232.16 KB)
1996 Archer M, Heitmeyer CL.  1996.  TAME: A Specialized Specification and Verification System for Timed Automata. Work in Progress session at RTSS. PDF icon ArcherHeitmeyer1996b.pdf (134.07 KB)
1995 Heitmeyer CL, Labaw B.  1995.  Consistency Checking of SCR-Style Requirements Specifications. International Symposium on Requirements Engineering. PDF icon HeitmeyerLabaw1995.pdf (257.28 KB)
1995 Heitmeyer CL, Bull A, Gasarch C, Labaw B.  1995.  SCR*: A Toolset for Specifying and Analyzing Requirements. Tenth Annual Conference on Computer Assurance (COMPASS '95). :109-122.PDF icon Heitmeyer etal1995.pdf (388.92 KB)
1995 McLean J, Heitmeyer CL.  1995.  High Assurance Computer Systems: A Research Agenda. America in the Age of Information, National Science and Technology Council Committee on Information and Communications Forum. PDF icon McLeanHeitmeyer1995.pdf (103.99 KB)
1994 Heitmeyer CL, Lynch N.  1994.  The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems. NRL Memorandum Report. PDF icon HeitmeyerLynch1994.pdf (242.1 KB)
1994 Heitmeyer CL, Lynch N.  1994.  The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems. IEEE Real-Time Systems Symposium. PDF icon HeitmeyerLynch1994b.pdf (311.85 KB)
1994 Heitmeyer CL.  1994.  The Role of HCI in CASE Tools Supporting Formal Methods. Workshop on Software Engineering an human-Computer Interaction. PDF icon Heitmeyer1994.pdf (16.11 KB)
1993 Clements P.C, Heitmeyer CL, Labaw B, Rose A.T.  1993.  MT: A toolset for specifying and analyzing real-time systems. IEEE Real-Time Systems Symposium. :12-22.PDF icon Clements etal1993.pdf (841.51 KB)
1993 Heitmeyer CL, Labaw B, Jeffords R.  1993.  A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems. Tenth IEEE Workshop on Real-Time Operating Systems and Software. PDF icon Heitmeyer etal1993.pdf (95.56 KB)