3 papers
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…
cs.SE2021
Verifying Verified Code
Siddharth Priya, Xiang Zhou, Yusen Su +3
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explo…