Abstract
Formulog extends Datalog with mechanisms for constructing logical terms and reasoning about them with satisfiability modulo theories (SMT) solving; a first-order functional language aids inspecting and manipulating complex terms. This combination of features makes it possible to write complex SMT-based program analyses in a way close to their formal specification, while being satisfactorily performant thanks to powerful Datalog optimizations and efficient evaluation techniques.
| Original language | English |
|---|---|
| Pages (from-to) | 48-53 |
| Number of pages | 6 |
| Journal | CEUR Workshop Proceedings |
| Volume | 3203 |
| State | Published - 2022 |
| Event | 4th International Workshop on the Resurgence of Datalog in Academia and Industry, Datalog-2.0 2022 - Genova-Nervi, Italy Duration: 5 Sep 2022 → … |
Keywords
- Datalog
- program analysis
- satisfiability modulo theories (SMT)
