mrefj

4 ms·

1.
by mrefj 8y ago
That is true. Scaling this to processor with caches and deep pipelines is completely non-trivial. There has been some attempt to scale to more "realistic" designs with compositional (stepwise) verification. http://www.c
2.
Refinement-based approach to reasoning of optimized reactive systems(ccs.neu.edu)
3 points by mrefj 8y ago|1 comments
3.
by mrefj 10y ago
ACL2 http://www.cs.utexas.edu/~moore/acl2/
4.
by mrefj 10y ago
> 1. Refinement mappings in TLA also allow arbitrary state functions. Could you please point me to a reference for this. The completeness result from "The existence of refinement mapping" only includes projection. I know that
5.
by mrefj 10y ago
> If you mean you want it to be automated ACL2 is an alternative that strives to strike a balance between interaction and automation. - It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, et
6.
by mrefj 10y ago
> My problem is that some reductions require moving certain transitions backwards or forwards in time. This is definitely a more involved problem. A cleaner solution, I believe, requires a new notion of correctness than trace containment
7.
by mrefj 10y ago
Thanks for the explanation especially with the example. I now understand what you meant by "unsound refinement" and the desire to keep the spec readable. > and that's what I did in a complex spec Do you believe that your h
8.
by mrefj 10y ago
> create a "refinement" mapping which isn't sound (and therefore isn't a refinement). Could you please illustrate what do you mean by unsound refinement ? Refinement mapping along with the notion of correctness forms
9.
by mrefj 10y ago
> But reasoning with functions is a specific level of abstraction. Excellent point. The level of abstraction is a fundamental concern, not just in modeling but also in reasoning about systems. And state machines (as used in TLA or otherw