Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (Technical Report)

Zhou, Yi; Shah, Amar; Lin, Zhengyao; Heule, Marijn; Parno, Bryan

doi:10.1184/R1/29207189.v1

Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (Technical Report)

report

posted on 2025-06-04, 19:28 authored by Yi ZhouYi Zhou, Amar ShahAmar Shah, Zhengyao LinZhengyao Lin, Marijn Heule, Bryan ParnoBryan Parno

This is a technical report in supplementary to the paper titled "Cazamariposas: Automated Instability Debugging in SMT-based Program Verification" at CADE-30 .This report includes extended examples and benchmark information not presented the conference paper.

Funding

SaTC: CORE: Small: Automating the End-to-End Verification of Security Protocol Implementations

Directorate for Computer & Information Science & Engineering

Find out more...

AFRL and DARPA Agreement FA8750-24-9-1000

Future Enterprise Security initiative at Carnegie Mellon CyLab

History

Date

2025-06-01

Usage metrics

Keywords

Program Verification Satisfiability Modulo Theories Proof Instability Proof Debugging

Licence

In Copyright

Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (Technical Report)

Funding

SaTC: CORE: Small: Automating the End-to-End Verification of Security Protocol Implementations

AFRL and DARPA Agreement FA8750-24-9-1000

Future Enterprise Security initiative at Carnegie Mellon CyLab

History

Date

Usage metrics

Categories

Keywords

Licence

Exports