Automatic Deduction Applied: Program Synthesis and Question Answering (by Richard Waldinger, slides):
1. Program Synthesis: extracting programs from proofs;
2. History on Automatic Deduction:
a. McCarthy's advice taker;
b. Slagle's deducum;
c. Amphion system used in planetary astronomy;
3. Question in natural language and based on deduction rather than statistical search (on which IBM Watson applies)
Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko, slides):
1. Summarization vs. Invariance :
a. For the case with procedure invocations;
b. Owicki / Gries Proof Rule;
c. Rely / Guarantee Proof Rule;
2. Type System in Programming Languages:
a. Well-typed programs can never go wrong;
b. Type Tree vs. Refinement Tree (PVS-friendly specification).
Exercise proposed by Shankar: use PVS to write the specification for 2b, and submit to him.
Static and Dynamic Analysis of Concurrent Programs (by Aarti Gupta, slides):
1. Context Bounded Analysis using Sequentialization;
2. Dynamic Analysis:
a. Preemptive Context Bounding;
b. Trace Based Verification;
c. Predicative Analysis;
3. Garbage Collection in C++11;
4. SMT-Based symbolic search:
a. based on Concurrent Static Single Assignment (CSSA) encoding;
b. Modular Analysis.
Lab (by Andrey Rybalchenko):
ARMC: http://www7.in.tum.de/~rybal/
My Comment: it can be easily screwed up writing a much longer horn-like constraint verification code, even for just 20 lines of source code with inter-procedure calls. Is there any related work or possibility to generate these constraints automatically?
Prof. from CAS commented: Horn Clause was under warm studying and researching during 1980s. Then people came to obstacles and put it on the shelf for a long time. Recently it returns to alive. Deepak has done a bunch of elegant stuffs, including Ideal Generation, etc.
PPT Karaoke for fun tonight.
No comments:
Post a Comment