Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Full-time research positions at the Naval Rese...


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

From: Elizabeth Leonard <elizabeth.leonard@nrl.navy.mil>
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@nrl.navy.mil). Please indicate in your email
that you are applying for a fulltime, permanent position.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:58):

From: Elizabeth Leonard via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Full-Time Computer Scientist Positions

(US Citizens only. Masters, Ph.D, or equivalent required.)

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 has openings for two full-time, permanent research positions. New
hires will initially support the section's currently funded efforts but will
be expected eventually to develop and obtain funding for their own research.

The objective of the section's research program is to develop formal,
mathematically-based methods, models, algorithms, theories and tools
supporting the construction and analysis of software and software systems.
The methods and tools provide critical support for the development of high
assurance software for systems, such as autonomous systems, secure systems,
and control software that must satisfy properties such as safety, fault
tolerance, timing, and security. Many formal methods and tools produced by
the section's research have been applied to practical Navy and other
industrial-strength systems. Current research projects in the section
include Application-Specific Security of Source Code, High Assurance
Cyber-Physical Systems, Using Formal Methods in Building a Space Robot, and
Formal Methods for Self-Securing Systems.

We are interested in candidates with expertise in one or more of the
following:

. formal modeling, analysis, verification, and validation of
autonomous systems, including those that include machine learning

. formal modeling, analysis, verification, and validation of
cyber-physical systems

. compositional techniques for model-based software specification and
analysis

. scenario-based synthesis of software models

. requirements elicitation methods and tools

. automatic test-case generation

. automatic code generation

. assurance cases for system safety and security

. verification techniques and tools: decision procedures, SMT solvers,
model checking, theorem proving

. design and use of automatable techniques for verification of system
properties of source code based on code assertions and procedure contracts

. combining methods from AI (e.g., machine learning) with formal
methods

. incremental/regression verification


Application Process


A Masters, Ph.D., or the equivalent is required. U.S. citizenship is
required.

Interested candidates should send a CV to Dr. Elizabeth Leonard
(elizabeth.leonard@nrl.navy.mil). Please indicate in your email that you are
applying for a full-time, permanent position.

view this post on Zulip Email Gateway (Aug 22 2022 at 21:08):

From: Elizabeth Leonard via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Full-Time Computer Scientist Positions
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 has multiple openings for full-time, permanent research
positions.  New hires will initially support the section’s currently
funded efforts but will be expected eventually to develop and obtain
funding for their own research.

The objective of the section’s research program is to develop formal,
mathematically-based methods, models, algorithms, theories and tools
supporting the construction and analysis of software and software
systems.  The methods and tools provide critical support for the
development of high assurance software for systems, such as autonomous
systems, secure systems, and control software that must satisfy
properties such as safety, fault tolerance, timing, and security.  Many
formal methods and tools produced by the section’s research have been
applied to practical Navy and other industrial-strength systems. 
Current research projects in the section include High Assurance
Cyber-Physical Systems, Using Formal Methods to Assure the Safety and
Correctness of AI Agents That Learn, Assured Development and Operation
of Autonomous Systems, Runtime Verification for Autonomous Systems that
Use AI, and Using Formal Methods in Building a Space Robot.

We are interested in candidates with expertise in one or more of the
following:
•    formal modeling, analysis, verification, and validation of
autonomous systems, including those that include machine learning
•    formal modeling, analysis, verification, and validation of
cyber-physical systems
•    combining methods from AI (e.g., machine learning) with formal methods
•    synthesis of runtime monitors from formal specifications
•    compositional techniques for model-based software specification and
analysis
•    scenario-based synthesis of software models
•    requirements elicitation methods and tools
•    automatic test-case generation
•    automatic code generation
•    assurance cases for system safety and security
•    verification techniques and tools: decision procedures, SMT
solvers, model checkers, theorem provers


Application Process


A Masters, Ph.D., or the equivalent is required. U.S. citizenship is
required.

Interested candidates should send a CV to Dr. Elizabeth Leonard
(elizabeth.leonard@nrl.navy.mil). Please indicate in your email that you
are applying for a full-time, permanent position.


Last updated: Apr 25 2024 at 08:20 UTC