sturdy

Haskell版本的Sturdy不再維護。堅固的項目已在Scala中重新完成，可在https://gitlab.rlp.net/plmz/sturdy.scala上找到。

結實的

Sturdy是在Haskell中創建聲音靜態分析的庫。靜態分析是在沒有實際運行程序的情況下生成有關計算機程序的信息的工具。靜態分析的示例是類型的檢查器，錯誤查找器（例如Java Findbugs），安全性分析（例如污染分析）以及用於編譯器優化的分析。

該項目著重於聲音靜態分析。如果分析的結果反映了程序的實際運行時行為，並且用戶可以依靠結果，則靜態分析是有聲音的。例如，如果用於編譯器優化的靜態分析不符合，則優化可能會改變程序的語義，從而導致運行時出乎意料的行為。為此，堅固的遵循抽象解釋者的組成聲音證明和可重複使用的組成部分的組成理論，以簡化靜態分析的聲音證明。

堅固將具體的解釋器和抽象解釋器（靜態分析）分配到通用解釋器中。該通用解釋器是由包含描述語言語義的原始操作的接口進行了參數化的，例如try ， catch ， finally是例外。然後，混凝土和抽象的解釋器通過實現這些界面來實例化通用解釋器。這種重組不僅消除了靜態分析實施時的不同關注點，而且簡化了其健全性的證明。更多詳細信息可以在我們的ICFP論文中找到。

堅固的允許從可重複使用的分析組件模塊化構建靜態分析。每個分析組件都封裝了單個分析問題，並且可以獨立於使用的分析來證明聲音。此外，分析理論組成部分可以確保靜態分析是正確的，如果其所有分析組件都是合理的，則可以確保靜態分析。這意味著分析開發人員只要重複使用聲音分析組件，就不必擔心聲音。更多細節可以在我們的OOPSLA紙中找到。

入門

要構建，請安裝堆棧構建工具，並從項目的根目錄中運行stack build 。

該堅固的項目目前包含以下語言的具體，抽象和通用口譯員：

• PCF ，一種高階功能語言
• 而有條件和循環的命令式語言
• 方案，LISP家族中的功能語言。
• Stratego ，一種用於程序轉換的語言
• Lambdajs ，JavaScript的中間表示
• Jimple ，一種適合靜態分析的Java字節碼（正在進行的工作）

要運行特定語言stack test sturdy-$(lang)測試

 stack test sturdy-pcf

出版品

基於組合的fixpoint算法，用於大步抽象解釋器
Sven Keidel，Sebastian Erdweg，TobiasHombücher
國際功能編程會議（ICFP）。 ACM，2023。 [PDF]

WebAssembly的模塊化抽象定義解釋器
Katharina Brandl，Sebastian Erdweg，Sven Keidel，Nils Hansen
歐洲面向對象編程會議（ECOP）。 ACM，2023。 [PDF]

一種系統的方法來抽像對程序轉換的解釋
Sven Keidel和Sebastian Erdweg。
驗證，模型檢查和抽象解釋（VMCAI）。施普林格，2020年。 [PDF]

抽象解釋的聲音和可重複使用的組件
Sven Keidel和Sebastian Erdweg。
面向對象的編程，系統，語言和應用程序（OOPSLA）。 ACM，2019 [PDF] [談話]

抽象口譯員的組成聲音證明
Sven Keidel，Casper Bach Poulsen和Sebastian Erdweg。
國際功能編程會議（ICFP）。 ACM，2018 [PDF] [談話]

致謝

堅固的項目是以下人員的共同努力（按字母順序排列）：

Casper Bach Poulsen，Jente Hidskes，Matthijs Bijman，SarahMüller，Sebastian Erdweg，Sven Keidel，TobiasHombücher，Wouter Raateland