Abstract
Static program analysis has become an essential tool for developers to find and avoid bugs as well as security vulnerabilities. This is particularly important for applications requiring formal verification, e.g., safety- or security-critical applications.We formalize and prove correct all the components needed to specify and perform static analysis based on the Datalog logic programming language, including the first known Isabelle formalization of stratified Datalog. In addition the existence of least solutions for any stratified Datalog program is established and proven. We demonstrate the usefulness of our formalization by further formalizing the general Bit-Vector Framework and prove correct four classic analyses in this framework.
| Original language | English |
|---|---|
| Title of host publication | SAC '24: Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing |
| Publisher | Association for Computing Machinery |
| Publication date | 2024 |
| Pages | 1731-1732 |
| ISBN (Electronic) | 979-8-4007-0243-3/24/04 |
| DOIs | |
| Publication status | Published - 2024 |
| Event | The 39th ACM/SIGAPP Symposium on Applied Computing - Avila, Spain Duration: 8 Apr 2024 → 12 Apr 2024 |
Conference
| Conference | The 39th ACM/SIGAPP Symposium on Applied Computing |
|---|---|
| Country/Territory | Spain |
| City | Avila |
| Period | 08/04/2024 → 12/04/2024 |
Keywords
- Datalog
- formal methods
- Isabelle
- Static analysis