10 citations · 11 across the 5 of their papers we have counts for
5 papers
Carnap Ten Years Later: Lessons Learned and Next Steps
Graham Leach-Krouse
The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000…
Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution
Caleb Helbling, Graham Leach-Krouse, Michael Crystal
Modern high-assurance software systems development favors memory safe languages such as SPARK (ADA) or Rust. However, developers often encounter non-memory safe code (e.g., C) in l…
cozy: Comparative Symbolic Execution for Binary Programs
Caleb Helbling, Graham Leach-Krouse, Sam Lasser +1
This paper introduces cozy, a tool for analyzing and visualizing differences between two versions of a software binary. The primary use case for cozy is validating "micropatches":…
Carnap: An Open Framework for Formal Reasoning in the Browser
Graham Leach-Krouse
This paper presents an overview of Carnap, a free and open framework for the development of formal reasoning applications. Carnap's design emphasizes flexibility, extensibility, an…
Yablo's Paradox And Arithmetical Incompleteness
Graham Leach-Krouse
In this short paper, I present a few theorems on sentences of arithmetic which are related to Yablo's Paradox as Gödel's first undecidable sentence was related to the Liar paradox.…