[isabelle] Full-time research positions at the Naval Research Laboratory

Full-Time Computer Scientist Positions
(US Citizens only)
Naval Research Laboratory
Center for High Assurance Computer Systems
Washington, DC 20375

The Software Engineering Section of NRL’s Center for High Assurance Computer Systems is looking to hire full-time, permanent members for its research staff. Persons hired will initially support ongoing funded efforts in the section, but will eventually be expected to develop, and obtain funding for, their own research programs.

The objective of the section’s research program is to develop formal, mathematically based methods, models, algorithms, theories, and tools supporting both the construction and analysis of software at different levels of abstraction, from requirements through code. Such methods and tools provide vital support for the development of high assurance software for systems, such as autonomous systems, security systems and devices, and control software, that must satisfy critical system properties such as safety, timing, fault tolerance, and security. Many of the formal-methods-based techniques and tools produced in the Section’s past research have been applied to real Navy systems.

Current research in the section includes:

Application-Specific Security of Source Code: This project is developing theory, methods, and tools for analyzing source code for application-specific security properties such as data separation, absence of undesirable information flows, nonbypassability of critical code, and proper memory sanitization. The research combines template-based specification of security properties with automatic generation and checking of assertions to verify that code satisfies the specified properties and to detect violations of those properties.

High Assurance Cyber-Physical Systems:This project is developing new theory, methods, and tools for model-based development of cyber-physical systems.All methods and tools developed in the project will be demonstrated on real systems, which may include unmanned vehicles and robots.

Applications of Formal Methods in Developing Real Critical Systems:

(1) Robotics: Formal-methods-based modeling and analysis techniques and tools are being applied to critical software components of a robot designed to service satellites in space. In addition to applying well-established formal analysis methods and tools, new analysis techniques and tools are being developed to provide assurance that the robot behaves safely and functions correctly.

(2) Secure Systems: Formal analysis methods and tools are being developed and applied to critical aspects of a framework for self-securing systems.

Application Process
U.S. citizenship is required.

Interested candidates should send a CV and cover letter to Dr. Elizabeth Leonard (elizabeth.leonard at nrl.navy.mil). Please indicate in your email that you are applying for a fulltime, permanent position.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.