Sandia National Laboratories Computer Scientist, Formal Verification Researcher (Experienced) in Livermore, California
For internal Sandia applicants, this is a backfill position and this position is promotion eligible.
We seek a strong technical contributor to help lead our research efforts in formal verification of hardware and software. This is a full-time opening for R&D Computer Science researchers who are experts in formal methods. The successful candidate will be a researcher at the experienced senior level who can demonstrate the necessary technical knowledge and skill base to build a successful research program, with a consistent record of excellence in formal methods and automated verification of hardware and software and the acumen to successfully expand this work portfolio in formal verification. Our researchers are expected to conduct innovative research, publish and present results in refereed journals and conferences, work in multidisciplinary teams, and seek out new and significant problems of national importance. Collaboration with multi-disciplinary teams (in our local Sandia Center in Livermore and across Sandia to our ASC partners at our New Mexico site in Albuquerque) is critical to successfully realizing these objectives. Some travel will be required.
On any given day, you may contribute to and lead activities in one or more of the following:
- Develop formal verification capabilities that leverage domain specific languages and support interfaces to standard open source model checkers and automated theorem provers
- Solve practical engineering problems with real-world data that involve symbolic execution and discrete-event simulations
- Engage our capability development efforts using your skills with Haskell, OCaml, Coq, Python, C Verilog, VHDL,Bluespec, NuSMV, TLA, Kami framework, binary analysis,and assembly languages
- Collaborate within a multi-disciplinary team to solve challenging digital assurance problems with national security impact
- Bachelor's and PhD degrees in Computer Science or a related STEM discipline plus at least two years’ relevant experience;
- Evidence of relevant and exceptional achievements in formal methods research, as demonstrated in the form of technical publications in refereed journals and conferences, patents, in the development of software verification tools, and/or in-depth knowledge and experience of formal verification toolchains and applications, and/or by leadership roles in professional organizations;
- Expertise in at least three of the following: model checking, logical inference, automated theorem proving, and domainspecific languages;
- Experience leading a collaborative research environment on problems in a variety of domains;
- Active U.S. DOE Q security clearance
Expertise in one or more of the following areas:
- Equivalence checking, symbolic execution, and discrete-event simulation;
- Proficiency with high-performance computing platforms;
- A background in solving practical problems in science and engineering that involve encounters with real-world data;
- Experience with the processes for obtaining and managing research funding to include building project teams, writing research proposals (including Laboratory Directed R&D proposals) and progress reports, and working with internal and external sponsors;
- Evidence of professional service to the community, such as service on program committees, workshop organization, and/or editorial work
Our department (Digital Foundations & Mathematics) develops and maintains multiple technical capabilities. We develop and apply tools for the formal verification of digital systems, for electrical modeling and simulation analyses, and we develop computing accelerators for extreme environments. We are always interested in candidates with cross-disciplinary skillsets who can contribute to one or more of our programs.
The formal verification activities include formal methods analysis of hardware and software; modeling and simulation of digital or software systems; synthesis of hardware (digital logic) or software to meet formal specifications; binary analysis (developing a custom lifter capability); and development of specialized software utilizing advanced mathematics to meet customer needs.
The electrical modeling and simulation work includes printed circuit board level analysis of new systems in extreme environments, development of new capabilities in Sandia’s internal PSPICE solver Xyce, and support for the Sandia device modelling teams.
Our work on computing accelerators includes both modeling and designing novel fault tolerant architectures and new analog neuromorphic in-memory computing accelerators.
Our department (Digital Foundations & Mathematics) consists mostly of PhDs with research backgrounds in computer science, analysis of programming languages and domain specific languages, high-performance computing, physics, electrical engineering, electrical circuit modeling & simulation & analysis, and neuromorphic computing architectures. We collaborate and team closely with organizations across Sandia and a broad spectrum of external partners.
Sandia National Laboratories is the nation’s premier science and engineering lab for national security and technology innovation, with teams of specialists focused on cutting-edge work in a broad array of areas. Some of the main reasons we love our jobs:
- Challenging work withamazingimpact that contributes to security, peace, and freedom worldwide
- Extraordinary co-workers
- Some of the best tools, equipment, and research facilities in the world
- Career advancement and enrichment opportunities
- Flexible schedules, generous vacations,strongmedical and other benefits, competitive 401k, learning opportunities, relocation assistance and amenities aimed at creating a solid work/life balance*
World-changing technologies. Life-changing careers. Learn more about Sandia at: http://www.sandia.gov
*These benefits vary by job classification.
Sandia is required by DOE to conduct a pre-employment drug test and background review that includes checks of personal references, credit, law enforcement records, and employment/education verifications. Applicants for employment need to be able to obtain and maintain a DOE Q-level security clearance, which requires U.S. citizenship. If you hold more than one citizenship (i.e., of the U.S. and another country), your ability to obtain a security clearance may be impacted.
Applicants offered employment with Sandia are subject to a federal background investigation to meet the requirements for access to classified information or matter if the duties of the position require a DOE security clearance. Substance abuse or illegal drug use, falsification of information, criminal activity, serious misconduct or other indicators of untrustworthiness can cause a clearance to be denied or terminated by DOE, resulting in the inability to perform the duties assigned and subsequent termination of employment.
All qualified applicants will receive consideration for employment without regard to race, color, religion, sex, sexual orientation, gender identity, national origin, age, disability, or veteran status and any other protected class under state or federal law.