|
|
|
|
|
|
by jeff_marshall
3484 days ago
|
|
|
There have been quite a few systems that can handle proofs of the kinds of propositions you list above using various different logical frameworks, programming languages, and automatic and/or user-guided proof assistants. That said, it's no small feat to do a correct translation from the semantics of a full, modern, programming language into the semantics of a SMT solver (which appears to be the primary back-end for deciding propositions in this tool). I'll have to go read the actual dissertation to see how far that goes and whether any escape-hatches for user guidance exist (tactics, manual term manipulation, etc.). I haven't yet found a tool that doesn't allow extensive user guidance to be all that effective for proving things about code/systems that are interesting (to me). |
|
|