3 papers
cs.LO2026
Verifiable Checks for Business Rule Consistency
Joseph Tafese, Milad Hooshyar, Sam Bayless +2
Maintaining consistency between natural language documentation of business rules and their evolving internal implementations is a significant challenge in large-scale systems. We p…
cs.LO2026
Show Me The Money: An Exercise in Proof-Driven Software Understanding
Joseph Tafese, Karthik Nukala, Hassen Saïdi +3
We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase,…
cs.LO2023
Btor2MLIR: A Format and Toolchain for Hardware Verification
Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel
Formats for representing and manipulating verification problems are extremely important for supporting the ecosystem of tools, developers, and practitioners. A good format allows r…