Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Internship opportunities at the Naval Research...


view this post on Zulip Email Gateway (Aug 22 2022 at 16:41):

From: Elizabeth Leonard <elizabeth.leonard@nrl.navy.mil>
Graduate and Undergraduate Internships
(U.S. 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 offering paid student internships for Summer 2018.
Several ongoing projects within the section, all in the general area of
formal methods for critical systems, have internships available for both
graduate and undergraduate students.

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.

We are interested in applicants with expertise in any of the following:

·formal modeling/specification of software and systems

·verification techniques and tools: decision procedures, SMT solvers,
model checkers, theorem provers

·integration of analysis tools

·simulation of physical dynamics, ROS, Gazebo, cosimulation of software
and physical/mechanical processes

·compositional model-based techniques for software construction and analysis

·construction and analysis of continuous & discrete timed models of
cyber-physical systems

·automatic generation of code assertions and procedure contracts

·incremental parsing

·incremental/regression verification

·programming in: C, Java, Python

·parser generation using Antlr

·MySQL database development

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.


Program Information and Application Process


U.S. citizenship is required.

Interested candidates should send a resume to Dr. Elizabeth Leonard
(elizabeth.leonard@nrl.navy.mil). Please indicate in your email that you
are applying for an internship position.


Last updated: Mar 29 2024 at 08:18 UTC