tag:blogger.com,1999:blog-5780206530047749771.post8765747301667359728..comments2014-06-22T11:10:45.531-07:00Comments on Life, the Universe and Math: Is your analysis concrete?J. Ian Johnsonhttp://www.blogger.com/profile/02510605633293210260noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-5780206530047749771.post-81793733310699824312013-02-20T11:34:14.178-08:002013-02-20T11:34:14.178-08:00I can understand that line of reasoning, but the c...I can understand that line of reasoning, but the correspondence in this case is not a hard one to show (reachability is preserved), and it gives people an operational understanding of the analysis' mechanics. The difficult proof shifts from the analysis' soundness (something that you put a lot of work into) to a less difficult proof of this correspondence. I know because I went through both kinds of proofs. It is because of this journey that I encourage people to put their cleverness into a concrete semantics, prove a correspondence, and then pointwise abstract. It helps intuition and keeps you honest about the workings of your algorithm; you can just run the concrete semantics on your test programs and not have results skewed by introduced approximations.J. Ian Johnsonhttps://www.blogger.com/profile/02510605633293210260noreply@blogger.comtag:blogger.com,1999:blog-5780206530047749771.post-54946124332845686452013-02-20T09:36:55.915-08:002013-02-20T09:36:55.915-08:00CFA2 does have a non-standard concrete semantics (...CFA2 does have a non-standard concrete semantics (Fig 2.4b, pg 11 of my diss. It was also in the ESOP paper). It is the same non-standard semantics Matt Might used in his dissertation. This semantics is easy to abstract to a finite-state analysis like kCFA. It is trickier to go to the abstract semantics of CFA2; that abstraction is not straightforward.<br /><br />This choice was intentional. I did not want to have a concrete semantics with a stack because I preferred to start from sth that has already been used by others. (I generally try to reuse as much prior work as possible; this makes it easier to show the delta of my work.) When you create a new concrete semantics, sm can come and ask "but how does this correspond to the other semantics people usually use," so then you have to go and do that proof.elgrecohttps://www.blogger.com/profile/04676182694703955011noreply@blogger.com