From invariant checking to invariant inference using randomized search. We describe a general framework c2i for generating an invariant inference procedure from an invariant checking procedure. Given a checker and a language of possible invariants, c2i generates an inference procedure that iteratively invokes two phases. The search phase uses randomized search to discover candidate invariants and the validate phase uses the checker to either prove or refute that the candidate is an actual invariant. To demonstrate the applicability of c2i , we use it to generate inference procedures that prove safety properties of numerical programs, prove non-termination of numerical programs, prove functional specifications of array manipulating programs, prove safety properties of string manipulating programs, and prove functional specifications of heap manipulating programs that use linked list data structures.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke: ICE-based refinement type discovery for higher-order functional programs (2020)
- Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun: A learning-based approach to synthesizing invariants for incomplete verification engines (2020)
- Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
- Sharma, Rahul; Aiken, Alex: From invariant checking to invariant inference using randomized search (2016)
- Sharma, Rahul; Aiken, Alex: From invariant checking to invariant inference using randomized search (2014) ioport