Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
From Invariant Checking to Invariant Inference Using Randomized Search
verfasst von : Rahul Sharma, Alex Aiken
Erschienen in: Computer Aided Verification
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.