« Details about AtelierB's Predicate Prover | Main | How to clip an eps in latex »
May 10, 2004
Counter Logic with Uninterprected Functions (CLU)
[Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions - Bryant, Lahiri, Seshia (ResearchIndex)] An interesting logic to which AtelierB's predicate prover can be compared.
CLU allows arithmetic expressions, functions from int to int, frunctions from int to bool and successor. I bet we could have done most of our proofs in CLU. The question is: how many CLU proofs wouldn't have been found using the PP in AtelierB?
Posted by jones at May 10, 2004 03:10 PM
Comments
Post a comment
Thanks for signing in, . Now you can comment. (sign out)
(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)