2.4. Hybrid PBT and verification🔗

To be designed..

Laurel allows bypassing the symbolic checking of properties in various ways:

• Assumptions

• Bodyless procedures

By bypassing the symbolic check, a concrete check (property-based testing) can be used instead. How exactly Laurel will guarantee a correct hand-off between concrete and symbolic property checking, is yet to be designed.