Buck Baskin on Nostr: nprofile1q…82suv Are you aware of nprofile1q…6gyrf ‘s work? It seems like tools ...
nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjv7pjw5vfcawhkh98r6cpgl2udafff4685z7yt0f4yv80yys60dsq82suv (nprofile…2suv) Are you aware of nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqf3nlrmpjja65pzmvlegyl27l0y2m007nncxttdwqndrejajvdzask6gyrf (nprofile…gyrf) ‘s work? It seems like tools like Alive2 (https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf) could be a good inspiration.
At a high level Alive uses a solver under the hood to prove that a simpler/faster implementation is equivalent to an original program, and it seems like this line of work could be a good analogy for proving a flag would be set or clear at a point in a particular program
At a high level Alive uses a solver under the hood to prove that a simpler/faster implementation is equivalent to an original program, and it seems like this line of work could be a good analogy for proving a flag would be set or clear at a point in a particular program