1/27/10:
We did a brief overview of Ross Tate's paper "Generating Compiler Optimizations from Proofs" from POPL '10 (http://doi.acm.org/10.1145/1706299.1706345). We discussed whether their proof generalization approach was more broadly applicable than compiler optimization. One idea we wanted to pursue further was whether this idea could be used to take user-provided test cases and extend them to more general proofs (or partial proofs) for a program. This may amount to path-specific proofs and it is possible that we could use the path enumeration work from Bill Harris' paper with Sriram and others from POPL '10 (http://doi.acm.org/10.1145/1706299.1706309).
We also want to look at related work that has been done along these lines by Rybalchenko ("From tests to proofs", http://dx.doi.org/10.1007/978-3-642-00768-2_24) which won ETAPS '09 best paper award. Google search for "proofs from tests" also brings up a paper from CMU and MSR ("Proofs from tests", http://doi.acm.org/10.1145/1390630.1390634).
Sriram suggested two approaches to proof generalization, 1) explicit solving for linear invariant and 2) parameterization of the test-specific proofs. This differs from the approach of Tate et al. which Evan described as "Lemma discovery", i.e., remembering the axioms used to prove a specific case and then applying these axioms in the same order to a more general case.
For Friday, 2/5, we plan to read and discuss Tate et al.
1/28/10: (Sriram Sankaranarayanan)
Other papers that could be related (not at all elementary)
1. Sriram Rajamani et al. Proofs from Tests. (http://research.microsoft.com/apps/pubs/default.aspx?id=70541)
2. Harris et al. POPL 2010 (http://www.cs.colorado.edu/~srirams/papers/popl10.html).
Some further ideas:
1. In our discussion, we focussed much on invariants. There are other applications that are equally compelling.
One such is to automatically annotate code based on the behavior observed from unit tests. By annotations, I mean
adding pre/post-conditions. Here is an example:
char * strcat(char * p, char * q){
int i;
if (!p || !q) return NULL;
for(; *p; ++p);
for(; *q; ++p,++q){
*q=*p;
}
}
What we want to generate is a precondition (Cf. Sankaranarayanan et al. ISSTA 2008 http://www.cs.colorado.edu/~srirams/papers/issta2008.html )
(p!= NULL /\
q != NULL /\
__alloc(p) >= 1+ __zero_sentinel(p) /\
__alloc(q) >= 1+__zero_sentinel(p) /\
__alloc(p) >= 1+ __zero_sentinel(p) + ___zero_sentinel(q))
Based on our disscussion yesterday, we assume that parameterized unit test cases are available. Our ISSTA paper gives some ideas on how test
harnesses can be built automatically for these types of programs.
Test 1: p = NULL, q = ...
Test 2: p=.. , q= NULL
Test 3: p != NULL, q != NULL, choose __alloc(p), __zero_sentinel(p), __alloc(q), __zero_sentinel(q).
For each run that does not crash, we use a symbolic execution to generate backward preconditions that
holds just for that run.
Take an example where p!= NULL, q!= NULL, __alloc(p) = 2, __zero_sentinel(p) = 1, __alloc(q)= 1, __zero_sentinel(q)=0
For this particular run, backward analysis gives us the path precondition
p!= NULL /\ q!= NULL /\ __alloc(p) > 1 /\ __alloc(q) > 1 /\ __alloc(p) > 1
This is good. But can we actually generalize this?
We can do so by parameterizing the "1" s in the precondition to be unknown
(linear) expressions on __alloc(p), __alloc(q), __zero_sentinel(p), __zero_sentinel(q)
and so on. We can then generate constraints on what the coefficients should be.
@Evan: Can we do something simular for the linked list or other types of data structures?
I would like to make this work generally on those domains too.
Have a nice day!
Sriram