Formulog: Datalog + SMT + FP

Aaron Bembenek, Michael Greenberg, Stephen Chong

Research output: Contribution to journalConference articlepeer-review

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 languageEnglish
Pages (from-to)48-53
Number of pages6
JournalCEUR Workshop Proceedings
Volume3203
StatePublished - 2022
Event4th 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)

Fingerprint

Dive into the research topics of 'Formulog: Datalog + SMT + FP'. Together they form a unique fingerprint.

Cite this