PV4 LCTDgenerates increasingly precise tests to pinpoint an error or prove program correct

Verifier for C programs

Application domain/field


They have implemented the DASH algorithm as a modification to the Lime Concolic Tester (LCT). The DASH algorithm tries to generate tests based on counterexamples found with CEGAR. Uses Z3. In 2016, it participated in only one category of SV-COMP because it only supported reachability properties and had limited language support.


License: MIT


Related papers

Last publication date

9 April 2016

Related tools

Other tools that participated in the BitVectorsReach category of SV-COMP 2016: 2LS, CBMC, Ceagle, CPAchecker, ESBMC, Forest, Impara, PAC-MAN, SeaHorn, SMACK+Coral, Symbiotic, Ultimate Automizer, UKojak

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.