formulog

公式

tl; dr：用優化的類似Datalog的語言編寫基於SMT的程序分析（符號執行者，改進類型Checkers等）。

事實證明，Datalog是一種用於實施一系列程序分析的有用語言，但是使用SMT求解的分析不能輕鬆地用傳統版本的DataLog編寫。配方儀通過通過增強DataLog來構建和理由的SMT公式以及一些一階功能編程以使生活更輕鬆的方法來填補這一空白。

為什麼要在格式中寫下基於SMT的分析？

1. 通過結合邏輯編程，功能編程和SMT求解，Formulog使得可以在數學規範級別（例如推理規則）上聲明地對許多分析進行編碼，從而縮小規範和實現之間的差距 - 並經常在規格中揭示錯誤！
2. 這種高級編碼使公式可以將高級優化應用於您的分析，例如自動並行化和目標定向評估。
3. 多虧了我們的公式到陣線編譯器，您可以自動生成分析的C ++版本，該版本利用高度優化的數據算法和數據結構。

感興趣的？有關更多信息，請查看Formulog Docs（也在文檔目錄中可用），包括有關入門的提示和語言參考。為了了解在配方中構建基於SMT的非平凡分析所涉及的內容，請查看我們在Formulog中實現改進類型檢查器的教程。

貢獻

歡迎對該項目的貢獻！請打開一個GitHub問題，然後將拉動請求鏈接到它。拉動請求必須在合併之前以Google Java格式進行。要重新格式化代碼，請運行mvn spotless:apply ；您還可以通過運行mvn spotless:check檢查是否一致（不重新格式化）。

許可和第三方圖書館

配方件以Apache 2.0許可發布。

該項目使用第三方庫。您可以生成這些庫的列表，並使用此命令下載其關聯的許可證：

 mvn license:download-licenses

生成的內容可以在target/generated-resources/目錄中找到。