The Digital Foundations & Mathematics team at Sandia National Laboratories develops and applies tools for the formal verification of digital systems, electrical modeling and simulation analysis, and computing accelerators for extreme environments. Our 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, and development of specialized software utilizing advanced mathematics. The electrical modeling and simulation work includes: printed circuit board analysis of new systems in extreme environments, development of new capabilities in Sandia’s internal PSPICE solver Xyce, and support for the Sandia device modeling teams. Our work on computing accelerators includes modeling and designing novel fault tolerant architectures and new analog neuromorphic in-memory computing accelerators. Our department consists mostly of researchers with backgrounds in computer science, programming languages, high-performance computing, physics, electrical engineering, electrical circuit modeling & simulation, and neuromorphic computing.
- K. Morris, C. Snook, T. S. Hoang, G. Hulette, R. Armstrong and M. Butler. Formal verification and validation of run-to-completion style state charts using Event-B. Innovations in Systems and Software Engineering (2022). [URL] [PDF] [Bib]
- K. Morris, C. Snook, T. S. Hoang, G. C. Hulette, R. Armstrong, and M. Butler. Refinement and Verification of Responsive Control Systems. In Rigorous State-Based Methods: 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020, Proceedings. Springer-Verlag, Berlin, Heidelberg, 272–277. [URL] [PDF] [Bib]
- S. D. Pollard, P. Johnson-Freyd, J. Aytac, T. Duckworth, M. J. Carson, G. C. Hulette, and C. B. Harrison. Quameleon: A Lifter and Intermediate Language for Binary Analysis. In Workshop on Instruction Set Architecture Specification (SpISA), pp. 1–4. Portland, OR, USA, Sep 2019. [URL] [PDF] [Bib] [Slides]
- P. Johnson-Freyd, J. Aytac and G. C. Hulette. Topos Semantics for a Higher-order Temporal Logic of Actions. In Applied Category Theory Conference (ACT). Oxford, UK, Jul 2019. [URL] [PDF] [Bib] [Slides] “Fans of hyperdoctrines will like this!” — John Baez
- P. Johnson-Freyd, G. C. Hulette, and Z. M. Ariola. Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System. In International Workshop on Formal Methods for Industrial Critical Systems. (AVoCS FMICS) 2016. Lecture Notes in Computer Science, vol 9933. Springer, Cham. [PDF] [URL] [Bib]
The Digital Foundations & Math department is always looking for talented interns, typically at the advanced undergraduate or graduate level. We mostly hire during the summer, but year-round internships may also be available. Interns from our department have historically gone on to work full-time at Sandia or to pursue prestigious opportunities and fellowships afterwards. (can we claim that as our success?) Suggested qualifications include experience in any of: functional programming (e.g., OCaml, Haskell), formal verification (e.g., proof assistants, SMT solvers, static analysis), and mathematics. (e.g., formal logical systems, category theory, type theory, proof theory, theoretical computer science) Please email a member of our team for more information.