About
Takes an LLVM based program (e.g., C) input
program and generates LLVM IR bitcode. Specifically, it performs the
pre-processing and optimization of the bitcode for verification
purposes.
Takes as input the optimized LLVM bitcode and
emits verification condition as Constrained Horn Clauses (CHC). The
middle-end is in charge of selecting encoding of the VCs and the
degree of precision.
Takes CHC as input and outputs the result of the
analysis. In principle, any verification engine that digests CHC
clauses could be used to discharge the VCs. Currently, SeaHorn
employs several SMT-based model checking engines based on
PDR/IC3. Complementary, SeaHorn uses the abstract
interpretation-based analyzer CRAB (A language-agnostic framework for abstract interpretation) for providing numerical
invariants.
Analysis techniques
(The way we prove things)
Publications
- S. Wesley, M. Christakis, J. A. Navas, R. J. Trefler, V. Wüstholz, and A. Gurfinkel. Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE. At VMCAI 2022.
- S. Priya, X. Zhou, Y. Su, Y. Vizel, Yuyan Bao, and A. Gurfinkel. Verifying Verified Code. At ATVA 2021.
- S. Wesley, M. Christakis, J. A. Navas, R. J. Trefler, V. Wüstholz, and A. Gurfinkel. Compositional Verification of Smart Contracts Through Communication Abstraction. At SAS 2021.
- A. Gurkinkel and J.A. Navas. Abstract Interpretation of LLVM with a Region-Based Memory Model. At VSTTE 2021.
- J. A. Navas, B. Dutertre, I. Mason. Verification of an Optimized NTT Algorithm. At VSTTE 2020.
- J. Kuderski, A. Gurfinkel and J.A.Navas. Unification-based Pointer Analysis without Oversharing. At FMCAD 2019.
- E. Gershuni, N. Amit, A. Gurfinkel, N. Narodytska, J. A. Navas, N. Rinetzky, L. Ryzhyk and M. Sagiv. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions . (Slides) At PLDI 2019.
- J. Gennari, A. Gurfinkel, T.Kahsai, J.A.Navas, and E.J.Schwartz. Executable Counterexamples in Software Model Checking . (Slides) At VSTTE 2018.
- A. Gurfinkel and J.A.Navas. A Context-Sensitive Memory Model for Verification of C/C++ Programs . (Slides) At SAS 2017.
- A. Gurfinkel: SeaHorn Tutorial.
- C. Urban, A. Gurfinkel, T.Kahsai. Synthesizing Ranking Functions from Bits and Pieces. At TACAS 2016.
- T.Kahsai, J.A.Navas, D. Jovanovic, M. Schaf. Finding Inconsistencies in Programs with Loops. At LPAR 2015. LNCS 9450, pp. 499-514, 2015.
- G.Gange, J.A.Navas, P.Schachte, H.Sondergaard, P.Stuckey. Exploiting Sparsity in Difference-Bound Matrices . At SAS 2016.
- G.Gange, J.A.Navas, P.Schachte, H.Sondergaard, P.Stuckey. An Abstract Domain of Uninterpreted Functions. At VMCAI 2016.
- A. Gurfinkel Algoritmic Logic-Based Verification with SeaHorn. Invited tutorial at SYNASC 2015.
- A. Komuravelli, N.Bjorner, A. Gurfinkel, K. McMillan. Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. At FMCAD 2015. IEEE, pp. 89-96, 2015.
- A.Gurfinkel, T.Kahsai, A. Komuravelli, J.A.Navas. The SeaHorn Verification Framework. At CAV 2015. LNCS 9206, pp. 343-361. 2015
- A.Gurfinkel, T.Kahsai, J.A.Navas. Algorithmic Logic-Based Verification. At ACM SIGLOG Newsletter, April 2015.
- A.Gurfinkel, T.Kahsai, J.A.Navas. SeaHorn: A Framework for Verifying C Programs (Competition Contribution). At TACAS 2015. LNCS 9035. pp 447-450. 2015
- A. Komuravelli, A.Gurfinkel, S.Chaki. SMT-Based Model Checking for Recursive Programs.. At CAV 2014. LNCS 8559, pp. 17-34. 2014
