[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
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
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