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 inmemory computing accelerators. Our department consists mostly of researchers with backgrounds in computer science, programming languages, highperformance computing, physics, electrical engineering, electrical circuit modeling & simulation, and neuromorphic computing.

J. M. Li, J. Aytac, P. JohnsonFreyd, A. Ahmed, and S. Holtzen. A nominal approach to probabilistic separation logic. In ThirtyNinth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, July 2024. To appear.
[arXiv]

J. M. Cohen and P. JohnsonFreyd. A formalization of core why3 in coq. Proceedings of the ACM on Programming Languages, 8(POPL), Jan. 2024.
[PDF]
[Bib]

S. D. Pollard, R. C. Armstrong, J. Bender, G. C. Hulette, R. S. Mahmood, K. Morris, B. C. Rawlings, and J. Aytac. Q: A Sound Verification Framework for Statecharts and Their Implementations. In Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for SafetyCritical Systems (FTSCS ’22), Dec 2022, Auckland, New Zealand. ACM, New York, NY, USA, 16–26.
[URL]
[PDF]
[Bib]
[Slides]

S. Nedunuri and D. R. Smith. Inferring Environment Assumptions in Model Refinement. In 11th Workshop on Synthesis (SYNT), 2022, Haifa, Israel.
[PDF]
[Bib]
[Slides]

K. Morris, C. Snook, T. S. Hoang, G. Hulette, R. Armstrong and M. Butler. Formal verification and validation of runtocompletion style state charts using EventB. 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 StateBased Methods: 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020, Proceedings. SpringerVerlag, Berlin, Heidelberg, 272–277.
[URL]
[PDF]
[Bib]

S. D. Pollard, P. JohnsonFreyd, 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), 1–4. Portland, OR, USA, Sep 2019.
[URL]
[PDF]
[Bib]
[Slides]

P. JohnsonFreyd, J. Aytac and G. C. Hulette. Topos Semantics for a Higherorder Temporal Logic of Actions. In Applied Category Theory Conference (ACT). Oxford, UK, Jul 2019.
[URL]
[PDF]
[Bib]
[Slides]

C. Seshadhri, A. M. Smith, Y. Vorobeychik, J. R. Mayo, and R. C. Armstrong. Characterizing shortterm stability for Boolean networks over any distribution of transfer functions. In Physical Review E 94, 012301.
[URL]
[PDF]
[Bib]

P. JohnsonFreyd, 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.
[URL]
[PDF]
[Bib]

J. R. Mayo, R. C. Armstrong, and G. C. Hulette. Leveraging abstraction to establish outofnominal safety properties. In Formal Techniques for SafetyCritical Systems (FTSCS), 72–186, Cham, 2016. Springer International Publishing.
[URL]
[PDF]
[Bib]

G. C. Hulette, R. C. Armstrong, J. R. Mayo, and J. R. Ruthruff. Theoremproving analysis of digital control logic interacting with continuous dynamics. Electronic Notes in Theoretical Computer Science, 317:71–83, 2015. The Seventh and Eighth International Workshops on Numerical Software Verification (NSV).
[URL]
[PDF]
[Bib]

J. R. Mayo, R. C. Armstrong, and G. C. Hulette. Digital system robustness via design constraints: The lesson of formal methods. In 2015 Annual IEEE Systems Conference (SysCon) Proceedings, 109–114. IEEE, April 2015.
[URL]
[PDF]
[Bib]

Z. J. Sullivan and S. D. Pollard. A formal model for portable, heterogeneous accelerator programming. Technical report, Sandia National Laboratories, 2024. To appear.
[PDF (with appendix)]
¶

S. D. Pollard, J. M. Aytac, A. Kellison, I. Laguna, S. Nedunuri, S. Reis, M. J. Sottile, and H. K. Thornquist. The first trilab workshop on formal verification: Capabilities, challenges, research opportunities, and exemplars. Technical report, Sandia National Laboratories, 2024.
[PDF]
¶

MC3 — Modal Mu Calculus Model Checking Using Myopic Constraints
[Tech Report]
[Github]

XStack KLOKKOS: Automated Test Generation for Performance Portable Programs Using Clang/LLVM and Formal Methods
[Github]
The Digital Foundations & Math team is always looking for talented interns at the advanced undergraduate or graduate level. We typically interview between DecemberFebruary for internships in the following summer, but yearround internships may also be available. Interns from our department have historically gone on to work fulltime 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.
Page last updated: 15 Aug 2024