Loading...
Please wait, while we are loading the content...
Program Extrapolation with Jennisys
| Content Provider | Microsoft Research |
|---|---|
| Author | Leino, K. Rustan M. Milicevic, Aleksandar |
| Copyright Year | 2012 |
| Abstract | The desired behavior of a program can be described using an abstractmodel. Compiling such a model into executable code requires advancedcompilation techniques known as synthesis. This paper presents alanguage, called Jennisys, where programming is done by introducing anabstract model, defining a concrete data representation for the model,and then being aided by automatic synthesis to produce executablecode. The paper also presents a synthesis technique for the language.The technique is built on an automatic program verifier that, via anunderlying SMT solver, is capable of providing concrete modelsto failed verifications. The technique proceeds by obtaining sampleinput/output values from concrete models and then extrapolating programs fromthe sample points. The synthesis aims to produce code withassignments, branching structure, and possibly recursive calls.A prototype of the language and synthesis technique has beenimplemented. |
| Issue Number | MSR-TR-2012-12 |
| Language | English |
| Publisher | Microsoft Technical Report |
| Publisher Date | 2012-02-01 |
| Access Restriction | Open |
| Rights Holder | Microsoft Corporation |
| Subject Keyword | Software development Programming principles Tools Languages |
| Content Type | Text |
| Resource Type | Training Manual |
