Proving or Disproving likely Invariants with Constraint Reasoning

Details Proving or Disproving likely Invariants with Constraint Reasoning Proving or Disproving likely Invariants with Constraint Reasoning

2005-08-24

arxiv.org/abs/cs/0508108v1

Computer Science

Software Engineering

In A. Serebrenik and S. Munoz-Hernandez (editors), Proceedings of the 15th Workshop on Logic-based methods in Programming Envi

Scientific paper

A program invariant is a property that holds for every execution of the program. Recent work suggest to infer likely-only invariants, via dynamic analysis. A likely invariant is a property that holds for some executions but is not guaranteed to hold for all executions. In this paper, we present work in progress addressing the challenging problem of automatically verifying that likely invariants are actual invariants. We propose a constraint-based reasoning approach that is able, unlike other approaches, to both prove or disprove likely invariants. In the latter case, our approach provides counter-examples. We illustrate the approach on a motivating example where automatically generated likely invariants are verified.

Affiliated with

Also associated with

No associations

Rating

Proving or Disproving likely Invariants with Constraint Reasoning does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Proving or Disproving likely Invariants with Constraint Reasoning, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Proving or Disproving likely Invariants with Constraint Reasoning will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-268881