Feedback Thread: DIP 1040--Copying, Moving, and Forwarding--Community Review Round 1

[Imperatorn]

On Monday, 8 March 2021 at 17:42:16 UTC, Timon Gehr wrote:
> On 08.03.21 15:01, Imperatorn wrote:
>> On Monday, 8 March 2021 at 11:28:53 UTC, Timon Gehr wrote:
>>> [...]
>> 
>> Just curious, is there any connection here to symbolic 
>> execution?
>
> Most program analysis is abstract interpretation in some way as 
> it is, well, abstract.
>
> You can consider symbolic execution as an abstract domain 
> consisting of symbolic formulas such that the concretization 
> function γ maps each symbolic formula to the set of program 
> states that satisfy it. Possible choices for meet and join are 
> symbolic conjunction and disjunction.
>
> Then, a fully precise abstract transformer f^# is a symbolic 
> transformer in the sense f[γ(φ)] = γ(f^#(φ)). If your symbolic 
> execution does not fully model some aspects of the program 
> semantics you will get the ordinary soundness condition f[γ(φ)] 
> ⊆ γ(f^#(φ)).
>
> Widening for this domain is invariant synthesis and if you do 
> it (automated or manually), you get something that's getting 
> close to what's usually called a program verifier instead of a 
> static analyzer.

Interesting. That sounds quite powerful. But what about 
undecidability? Wait... The abstract semantics is a super set 
here right? Hmm, so that's why that works.

This is actually kinda cool.

Do you have any good books on the subject to recommend?