Screenshot

Biographical information

  • Currently, Senior Formal Methods Researcher/Directorate Fellow at Idaho National Laboratory
  • Formerly, Senior Principal Research Scientist at Two Six Technologies
  • Formerly, Senior Cybersecurity Research Scientist at Oak Ridge National Laboratory
  • Formerly, Associate Professor of Computer Science at the University of Missouri
  • Recipient: NSF CAREER Award 2008 (CyberTrust program)
  • Post-doctoral Researcher at Oregon Graduate Institute from June 2000-August 2003
  • Visiting Lecturer (Computer Science), Indiana University, September 1999-May 2000
  • Ph.D (Computer Science), University of Illinois at Urbana-Champaign 2001
  • M.S. (Computer Science), University of California at Davis, August, 1992
  • B.A. (Mathematics), University of California at Berkeley, May 1986

Research Interests

Language-based methods in computer security, all aspects of programming languages design and implementation, functional high-level synthesis, Computer and information security, malware analysis, and formal methods.

Contact Information

Recent Publications

  • Temporal Staging for Correct-by-Construction Cryptographic Hardware., Yakir Forman and Bill Harrison. Proceedings of the 2024 Rapid Systems Prototyping (RSP24). pdf
  • Formalized High Level Synthesis with Applications to Cryptographic Hardware., Bill Harrison, Ian Blumenfeld, Eric Bond, Chris Hathhorn, Paul Li, May Torrence, and Jared Ziegler. Proceedings of the 2023 NASA Formal Methods Symposium (NFM23). pdf
  • A Mechanized Semantic Metalanguage for High Level Synthesis., Bill Harrison, Chris Hathhorn, and Gerard Allwein. Proceedings of PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming. pdf code
  • Strongly Bounded Termination with Applications to Security and Hardware Synthesis., Tom Reynolds, Rohit Chadha, Bill Harrison, and Gerard Allwein. Proceedings of TyDe 2020: ACM Workshop on Type Driven Development. pdf
  • Verifiable Security Templates for Hardware., Bill Harrison and Gerard Allwein. Proceedings of 2020 Design, Automation, and Test Europe (DATE). pdf
  • Language Abstractions for Hardware-based Control-Flow Integrity Monitoring. Bill Harrison and Gerard Allwein. Proceedings of the 2018 International Conference on Reconfigurable Computing and FPGAs. pdf codebase
  • The Mechanized Marriage of Effects and Monads with Applications to High Assurance Hardware. Tom Reynolds, Bill Harrison, Adam Procter, and Gerard Allwein. ACM Transactions on Embedded Computing Systems (Feb 2019). pdf
  • Semantics-directed Prototyping of Hardware Runtime Monitors. Bill Harrison and Gerard Allwein. Proceedings of the 29th International Symposium on Rapid System Prototyping (RSP). pdf
  • A Core Calculus for Secure Hardware: Its Formal Semantics and Proof System. Tom Reynolds, Adam Procter, Bill Harrison, and Gerard Allwein. 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE17). pdf
  • A Programming Model for Reconfigurable Computing Based in Functional Concurrency, William L. Harrison, Adam Procter, Ian Graves, Michela Becchi, and Gerard Allwein. ReCoSoC 2016 pdf slides.
  • Provably Correct Development of Reconfigurable Hardware Designs via Equational Reasoning, Ian Graves, Adam Procter, William L. Harrison, and Gerard Allwein. FPT 2015 pdf slides.
  • A Principled Approach to Secure Multi-Core Processor Design with ReWire, Adam Procter, William Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. ACM Transactions on Embedded Computing Systems pdf.
  • Semantics Driven Hardware Design, Implementation, and Verification with ReWire, Adam Procter, William Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. LCTES 2015 pdf.
  • Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation, Ian Graves, Adam Procter, William Harrison, Michela Becchi, and Gerard Allwein. ARC 2015 pdf.