3 papers
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.SE2024
Unlocking the Power of Environment Assumptions for Unit Proofs
Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel
Clearly articulating the assumptions of the execution environment is crucial for the successful application of code-level formal verification. The process of specifying a model for…
cs.PL2024
Ownership in low-level intermediate representation
Siddharth Priya, Arie Gurfinkel
The concept of ownership in high level languages can aid both the programmer and the compiler to reason about the validity of memory operations. Previously, ownership semantics has…