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)