2 papers
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…
cs.PL2020
Data Flow Refinement Type Inference
Zvonimir Pavlinovic, Yusen Su, Thomas Wies
Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of cons…