Ranking function synthesis for bit-vector relations
<p style="text-align:justify;">Ranking function synthesis is a key component of modern termination provers for imperative programs. While it is well-known how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking...
Main Authors: | Cook, B, Kroening, D, Rummer, P, al., E |
---|---|
Format: | Journal article |
Published: |
Springer
2013
|
Similar Items
-
Ranking function synthesis for bit-vector relations
by: Cook, B, et al.
Published: (2010) -
Approximating Predicate Images for Bit−Vector Logic
by: Kroening, D, et al.
Published: (2006) -
Deciding Bit−Vector Arithmetic with Abstraction
by: Bryant, R, et al.
Published: (2007) -
Unrestricted termination and non-termination arguments for bit-vector programs
by: David, C, et al.
Published: (2015) -
Synthesis of domain specific CNF encoders for bit-vector solvers
by: Inala, Jeevana Priya
Published: (2016)