Korn—Software Verification with Horn Clauses (Competition Contribution)
Author:
Open Access
- 20 April 2023
- book chapter
- Published by Springer Nature
- p. 559-564
Abstract
Korn is a software verifier that infers correctness certificates and violation witnesses sutomatically using state-of-the-art Horn-clause solvers, such as Z3 and Eldarica. The solvers are used in a portfolio together with cheap random sampling where the latter can be very effective at finding counterexamples. Korn perfomend best in the sub-category of SV-COMP 2023.Keywords
This publication has 8 references indexed in Scilit:
- Competition on Software Verification and Witness Validation: SV-COMP 20232023
- Loop Verification with Invariants and Contracts2022
- The Science, Art, and Magic of Constrained Horn Clauses2019
- The ELDARICA Horn Solver2018
- Horn Clause Solvers for Program Verification2015
- The SeaHorn Verification Framework2015
- On Solving Universally Quantified Horn Clauses2013
- Specified BlocksLecture Notes in Computer Science, 2008