ICSE 2026 (series) / FormaliSE 2026 (series) / Research Track /
Toward an automatic formal verification of Cairo v0 programs (Extended Abstract)
Mon 13 Apr 2026 14:45 - 15:00 at Oceania VIII - Session 5: Automated Reasoning, and Program Analysis
This article presents a deductive program verifier for Cairo v0, designed to automate the verification of key properties in Cairo v0 programs while minimizing manual effort. Our tool transpiles Cairo v0 programs into the formal intermediate language Boo- gie, enabling static analysis and SMT-based proof generation. We demonstrate its capability to automatically verify properties com- monly exhibited in blockchain-based programs.
Mon 13 AprDisplayed time zone: Brasilia, Distrito Federal, Brazil change
Mon 13 Apr
Displayed time zone: Brasilia, Distrito Federal, Brazil change
14:00 - 15:30 | Session 5: Automated Reasoning, and Program AnalysisResearch Track / FormaliSE Program at Oceania VIII | ||
14:00 30mTalk | Profile-Guided Constraint Simplification for Symbolic Execution Research Track Roxana Shajarian University of Nebraska-Lincoln, Md Rashedul Hasan University of Nebraska-Lincoln, Lisong Xu University of Nebraska-Lincoln, USA, Hamid Bagheri University of Nebraska-Lincoln | ||
14:30 15mTalk | BPMN-T: A Timed–Probabilistic Extension of BPMN with Formal Semantics Research Track Ahang Zuo Univ. de Pau et des Pays de l’Adour | ||
14:45 15mTalk | Toward an automatic formal verification of Cairo v0 programs (Extended Abstract) Research Track | ||