Adam Petz

Recent Posts

Blog Categories


A blog for thoughts, technical discussions, announcements.

MEMOCODE Paper Accepted

30 Aug 2021

“Design and Formal Verification of a Copland-based Attestation Protocol” by Adam Petz, Grant Jurgensen, and Perry Alexander has been accepted for publication at the MEMOCODE ‘21 conference, Nov 20-22, to be held virtually. This paper introduces a workflow for both analyzing and executing Copland-based attestation protocols in the context of a security architecture. It concludes by instantiating that workflow with a concrete architecture and layered attestation protocol designed for a DARPA CASE demonstration platform that hosts a legacy UAV flight control application. Here is a link to the camera-ready pdf.


NFM ‘21 (Virtual) Conference Presentation

28 May 2021

I recently presented our work entitled “An Infrastructure for Faithful Execution of Remote Attestation Protocols” at the (virtual) NASA Formal Methods (NFM’21) conference. A video recording of my talk/slides and live Q&A following the talk can be viewed on Youtube here. Here is a link to a pdf of the published paper.


Paper Accepted to NFM ‘21

24 Feb 2021

Our paper entitled “An Infrastructure for Faithful Execution of Remote Attestation Protocols” was accepted to appear in the upcoming NASA Formal Methods conference. I will present this work (virtually) during the conference program in May, 2021. Here is a link to the published pdf.


Ltac Bug or Ltac Feature?

07 Dec 2020

I encountered some surprising (to me) behavior while writing an Ltac procedure involving a “with” clause. A minimal example appears below. The problem occurs when binding a variable from a hypothesis, then using that variable in the LHS of a with binding in the Ltac body. My expectation is that the LHS (x in the assignment x:=y) is unaffected by substitution, and must simply match the name of a bound variable in the type of the Lemma to which it is being applied.


Deep Field by Eric Whitacre

07 Dec 2020

I’ve been listening to “Deep Field” by Eric Whitacre. Inspired by the Hubble Telescope’s Deep Field image. I’d recommend listening on a music streaming service for best sound quality, but here’s a site with a description and companion video with Hubble images:


Higher-Order Automation

24 Nov 2020

I would like to pass a tactic as a parameter to a separately-defined Ltac procedure. However, it seems whenever I include a “;” in that tactic I’m met with a syntax error. I’ve crafted a minimal example below. Perhaps I’ve made a silly mistake with parentheses or some such, but I can’t seem to get it working.

Ltac my_tac tac := tac.
Lemma foo : (1 = 1 /\ 2 = 2).
  split; [reflexivity | reflexivity]. (* Succeeds as expected *)
  my_tac (split; [reflexivity | reflexivity]).  (* Syntax Error? *)


HotSoS 2020 Poster Presentation

22 Sep 2020

Gave a virtual poster presentation at HotSoS 2020 entitled: “An Infrastructure for Faithful Execution of Remote Attestation Protocols”. The poster pdf is here, and the accompanying 3-minute lightning talk presentation here. Fielded live questions from the audience via video chat after.


Dissertation Proposal Defense

14 Aug 2020

Passed the oral defense component of my dissertation proposal entitled: “An Infrastructure for Faithful Execution of Remote Attestation Protocols”. Now on to more publications and defending the dissertation!


HotSoS 2019 Paper Presentation

12 Apr 2019

Successfully presented our work entitled “A Copland Attestation Manager” published at HotSoS 2019 (Hot Topics in Science of Security) in Nashville, TN. Watch the presentation on YouTube here: The work is co-authored with my advisor, Dr. Perry Alexander, and the full paper can be found here: link to pdf.