BibSonomy publications for /user/emanuel/aseThu Sep 04 16:42:23 CEST 2008Los Alamitos, CA, USAIEEE Transactions on Software Engineering3141--153Constructing Programs from Example Computations21976pre-summers program_synthesis ase induction synthesis_from_traces inductive_programming An autoprogrammer is an interactive computer programming system which automatically constructs computer programs from example computations executed by the user. The example calculations are done in a scratch pad fashion at a computer display using a light pen or other graphic input device, and the system stores a detailed history of all of the steps executed in the process. Then the system automatically synthesizes the shortest possible program which is capable of executing the observed examples. The paper describes the computational environment provided by the system, proves that the program synthesis technique is both "sound" and "complete," describes the design of the system, and gives some programs it was used to create.Sun Apr 20 17:55:17 CEST 2008Automated Software Engineering2167--193Logic Program Synthesis as Problem Reduction Using Combining Forms82001program_synthesis inductive_programming combinduce combilog article induction enumerative_ip ase ilp recursion_schemes This paper presents an approach to inductive synthesis of logic programs from examples using problem decomposition and problem reduction principles. This is in contrast to the prevailing logic program induction paradigm, which relies on generalization of programs from examples. The problem reduction is accomplished as a constrained top-down search process, which eventually is to reach trivial problems.Fri Apr 18 17:43:10 CEST 2008New York, NY, USAJournal of Systems and Software3275--296Specifications are necessarily informal or: some more myths of formal methods401998article comparison formal_methods program_synthesis ase software_engineering position_paper Fri Apr 18 17:29:28 CEST 2008Automated Software Engineering2131--137Inductive Programming82001ase inductive_programming induction program_synthesis article software_engineering position_paper Thu Apr 17 12:36:17 CEST 2008New York, NY, USAJournal of the ACM144--67A Transformation System for Developing Recursive Programs241977article deductive_program_synthesis program_optimisation program_synthesis ase program_transformation A system of rules for transforming programs is described, with the programs in the form of recursion equations. An initially very simple, lucid, and hopefully correct program is transformed into a more efficient one by altering the recursion structure. Illustrative examples of program transformations are given, and a tentative implementation is described. Alternative structures for programs are shown, and a possible initial phase for an automatic or semiautomatic program-manipulation system is indicated.Thu Apr 17 12:29:00 CEST 2008New York, NY, USAACM Transactions on Programming Languages and Systems190--121A Deductive Approach to Program Synthesis21980ase article deductive_program_synthesis program_synthesis Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.Wed Apr 16 16:23:42 CEST 2008KES.U.01.3.{SPECWARE} - Producing Software Correct by Construction2001program_synthesis techreport deductive_program_synthesis software_engineering specware kestrel ase Wed Apr 16 16:14:46 CEST 2008Formal Methods at the Crossroads: From Panacea to Foundational Support267--286LNCSSoftware Development by Refinement27572003ase deductive_program_synthesis program_synthesis overview kestrel software_engineering inproceedings This paper presents an overview of the technical foundations and current directions of Kestrel’s approach to mechanizing software development. The approach emphasizes machine-supported refinement of property-oriented specifications to code, based on a category of higher-order specifications. A key idea is representing knowledge about programming concepts, such as algorithm design, and datatype refinement by means of taxonomies of design theories and refinements. Concrete refinements are generated by composing library refinements with a specification. The framework is partially implemented in the research systems Specware, Designware, Epoxi, and Planware. Specware provides basic support for composing specifications and refinements via colimit, and for generating code via logic morphisms. Specware is intended to be general-purpose and has found use in industrial settings. Designware extends Specware with taxonomies of software design theories and support for constructing refinements from them. Epoxi builds on Designware to support the specification and refinement of systems. Planware transforms behavioral models of tasks and resources into high-performance scheduling algorithms. A few applications of these systems are presented. ER -