Jan :rust: :ferris:
@janriemer@floss.social  ·  activity timestamp 4 weeks ago

ESBMC - An Efficient SMT-based Bounded Model Checker

https://ssvlab.github.io/esbmc/

"ESBMC is an open-source, [...], context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well."

1/3

#SMT#FormalVerification#FormalMethods#ModelChecking
Jan :rust: :ferris:
@janriemer@floss.social replied  ·  activity timestamp 4 weeks ago
#LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling

https://dl.acm.org/doi/10.1145/3691620.3695512

"We investigate a modification of the classical Bounded Model Checking (BMC) procedure that does not handle loops through unrolling but via modifications to the control flow graph (CFG). A portion of the CFG representing a loop is replaced by a node asserting invariants of the loop[...]."

(continues next toot...)

2/3

#LLMs #AI #ArtificialIntelligence
Jan :rust: :ferris:
@janriemer@floss.social replied  ·  activity timestamp 4 weeks ago

"[...]Our experimental results show that the resulting tool, ESBMC ibmc, is competitive with state-of-the-art formal verifiers for programs with unbounded loops, significantly improving the number of programs verified by the industrial-strength software verifier ESBMC and verifying programs that state-of-the-art software verifiers such as SeaHorn and VeriAbs could not."

3/3