Rights accessRestricted access - confidentiality agreement
We consider the problem of generating program invariants to prove safety, focusing on invariants that belong to difference logic (i.e., of the form x-y <= k). We present two new methods based on satisfiability modulo theories and constraint solving with promising experimental results.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: firstname.lastname@example.org