Digital Foundations & Mathematics

picture of a string of 0s and 1s under a magnifying glass


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.

Selected Works

Publications

  1. A. Dario and S. D. Pollard. A step-function abstract domain for granular floating-point error analysis. In 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, NSAD ’24. ACM, Oct. 2024. [URL] [PDF] [Bib]
  2. J. M. Li, J. Aytac, P. Johnson-Freyd, A. Ahmed, and S. Holtzen. A nominal approach to probabilistic separation logic. In Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, July 2024. [URL] [arXiv] [Bib]
  3. J. M. Cohen and P. Johnson-Freyd. A formalization of core why3 in coq. Proceedings of the ACM on Programming Languages, 8(POPL), Jan. 2024. [URL] [PDF] [Bib]
  4. 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 Safety-Critical Systems (FTSCS ’22), Dec 2022, Auckland, New Zealand. ACM, New York, NY, USA, 16–26. [URL] [PDF] [Bib] [Slides]
  5. S. Nedunuri and D. R. Smith. Inferring Environment Assumptions in Model Refinement. In 11th Workshop on Synthesis (SYNT), 2022, Haifa, Israel. [PDF] [Bib] [Slides]
  6. 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]
  7. 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]
  8. 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), 1–4. Portland, OR, USA, Sep 2019. [URL] [PDF] [Bib] [Slides]
  9. 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]
  10. C. Seshadhri, A. M. Smith, Y. Vorobeychik, J. R. Mayo, and R. C. Armstrong. Characterizing short-term stability for Boolean networks over any distribution of transfer functions. In Physical Review E 94, 012301. [URL] [PDF] [Bib]
  11. 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. [URL] [PDF] [Bib]
  12. J. R. Mayo, R. C. Armstrong, and G. C. Hulette. Leveraging abstraction to establish out-of-nominal safety properties. In Formal Techniques for Safety-Critical Systems (FTSCS), 72–186, Cham, 2016. Springer International Publishing. [URL] [PDF] [Bib]
  13. G. C. Hulette, R. C. Armstrong, J. R. Mayo, and J. R. Ruthruff. Theorem-proving 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]
  14. 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]

Technical Reports

  • Z. J. Sullivan and S. D. Pollard. A formal model for portable, heterogeneous accelerator programming. Technical report, Sandia National Laboratories, 2024. To appear. [URL] [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 tri-lab workshop on formal verification: Capabilities, challenges, research opportunities, and exemplars. Technical report, Sandia National Laboratories, 2024. [PDF] [Bib]

Open-Source Software

  • MC3 — Modal Mu Calculus Model Checking Using Myopic Constraints [Tech Report] [Github]
  • X-Stack KLOKKOS: Automated Test Generation for Performance Portable Programs Using Clang/LLVM and Formal Methods [Github]

Internships

The Digital Foundations & Math team is always looking for talented interns at the advanced undergraduate or graduate level. We typically interview between December-February for internships in the following 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.

Page last updated: 30 Sep 2024