SeaHorn Blog

Scribbling the ins and outs of an automated code analysis tool.

• Rust SmallVec Memory Leak 31 August 2023
• Rust SmallVec Insert Optimization 31 August 2023
• Rust SmallVec Grow Error 31 August 2023
• Rust SmallVec Drain Error 31 August 2023
• Rust SmallVec Buffer Overflow 31 August 2023
• Rust SmallVec 31 August 2023
• Loop Unrolling 21 July 2023
• Alignment Issues 21 July 2023
• Rust TinyVec Remove Error 12 July 2023
• Rust TinyVec 12 July 2023
• Custom Print Macros in Rust 12 July 2023
• Rust TinyVec Capacity Error 10 July 2023
• Handling Client Interference in SmartACE 17 July 2020
• Reasoning About Client State in SmartACE 15 June 2020
• Verifying Client Properties in SmartACE 08 June 2020
• Debugging Smart Contracts with SmartACE 08 June 2020
• Finding Representation Invariants for Smart Contracts 08 June 2020
• SmartACE: A Solidity Verification Framework 08 June 2020
• Static Analysis of Linux Kernel Extensions (aka eBPF programs) 04 July 2019
• Proving Equivalence of x86 programs with McSema + SeaHorn (III) 12 December 2018
• Proving Equivalence of x86 programs with McSema + SeaHorn (II) 12 December 2018
• Proving Equivalence of x86 programs with McSema + SeaHorn (I) 12 December 2018
• Executable Counterexamples in Software Model Checking 03 August 2018
• Using SeaHorn with Docker 24 February 2018
• A Context-Sensitive Memory Model for Verification of C/C++ Programs 01 October 2017
• Abstract Interpretation engine in SeaHorn 29 May 2017
• A different backend solver for SeaHorn 28 May 2017
• Proving Memory Safety with SeaHorn 27 May 2017
• A basic use of SeaHorn 20 May 2017
• Bug validation via test harness 16 October 2016
• Installing SeaHorn 14 October 2016