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 → … |
UN SDGs
This output contributes to the following UN Sustainable Development Goals (SDGs)
-
SDG 3 Good Health and Well-being
Keywords
- Datalog
- program analysis
- satisfiability modulo theories (SMT)
Fingerprint
Dive into the research topics of 'Formulog: Datalog + SMT + FP'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver