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

Verifier for C programs

Application domain/field

• Symbolic execution
• Dynamic symbolic execution (DSE)
• Counterexample guided abstraction refinement (CEGAR)
• Reachability properties
• Assertion violations

Internals

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.

Comments

License: MIT