• Oyster

  • Referenced in 32 articles [sw19629]
  • Theorem proving and program synthesis with Oyster. Martin-Löf type theory provides a formal framework ... construction of verified programs, both specified and written in the type theory. We describe ... approach. We illustrate this by describing the synthesis of a simple evaluator of arithmetic expressions...
  • ROSETTA

  • Referenced in 23 articles [sw10969]
  • programming environments for process-oriented synthesis of logic programs...
  • SYMBA

  • Referenced in 11 articles [sw08528]
  • uses for them in software verification, program synthesis, functional programming, refinement types...
  • PRIZ

  • Referenced in 8 articles [sw29713]
  • combines conventional programming technique with automatic synthesis of programs from specifications. It enables ... used by the system for the program synthesis. PRIZ is not bound to any particular ... problem domain, but applicable for synthesis of programs solving problems of a wide class called...
  • FlashMeta

  • Referenced in 5 articles [sw29484]
  • FlashMeta: a framework for inductive program synthesis. Inductive synthesis, or programming-by-examples ... operator. This observation enables a novel program synthesis methodology called data-driven domain-specific deduction...
  • MAHA

  • Referenced in 7 articles [sw15809]
  • MAHA: A program for datapath synthesis. MAHA is a program which implements an algorithm ... register level synthesis of data paths from a data flow specification. The algorithm is based ... least scheduling freedom are scheduled first. The program either minimizes cost, subject to a time...
  • Amphion

  • Referenced in 5 articles [sw09953]
  • also serves to document the specification. Program synthesis is based upon constructive theorem proving...
  • GME

  • Referenced in 5 articles [sw33604]
  • creating domain-specific modeling and program synthesis environments. The configuration is accomplished through metamodels specifying...
  • LYaPAS

  • Referenced in 6 articles [sw32275]
  • Representation of Synthesis Algorithms, or LYaPAS (ЛЯПАС), is a programming language that sprung ... theoretical considerations oriented toward the programming of synthesis algorithms for finite-state and discrete devices...
  • TerpreT

  • Referenced in 2 articles [sw29483]
  • study machine learning formulations of inductive program synthesis; given input-output examples ... domain-specific language for expressing program synthesis problems. TerpreT is similar to a probabilistic programming ... discrete satisfiability solving, and the Sketch program synthesis system. We illustrate the value of TerpreT ... learning community to make progress on program synthesis...
  • APTS

  • Referenced in 4 articles [sw03405]
  • Program synthesis from formal requirements specifications using APTS...
  • Rosette

  • Referenced in 4 articles [sw27566]
  • extends Racket with language constructs for program synthesis, verification, and more. To verify or synthesize...
  • SemFix

  • Referenced in 4 articles [sw17449]
  • symbolic execution, constraint solving and program synthesis. In our approach, the requirement on the repaired ... compare our method with recently proposed genetic programming based repair on SIR programs with seeded...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • example, features of the system like argument synthesis and universe polymorphism make proof checking more ... language for formalization of mathematical problems and program specification and development...
  • SNARK

  • Referenced in 4 articles [sw19611]
  • unification algorithms, sorts, answer construction for program synthesis, procedural attachment, and extensibility by Lisp code...
  • AutoBayes/CC

  • Referenced in 4 articles [sw01806]
  • AutoBayes/CC -- combining program synthesis with automatic code certification -- system description. Code certification is a lightweight...
  • Sehwa

  • Referenced in 9 articles [sw08111]
  • described, and Sehwa, a program that performs such synthesis, is presented. The task includes...
  • MCGP

  • Referenced in 14 articles [sw00562]
  • based on our synthesis approach combining deep Model Checking and Genetic Programming. Given ... syntactic building blocks, the structure of the programs, and the fitness function, and to follow ... their effect on the convergence of the synthesis process...
  • NUT

  • Referenced in 2 articles [sw29714]
  • based programming with facilities for automatic program synthesis. The system allows to specify computational problems ... solved using algorithms for automatic program synthesis described earlier for the PRIZ system...
  • SKIL

  • Referenced in 2 articles [sw25433]
  • interactive theorem prover dedicated to program synthesis and implemented in Quintus- Prolog. The object-level ... proof search. These extracted terms are programs following the programming with proofs paradigm, having ... system is in fact a program synthesis environment, since a specification can be regarded ... proposition and its extracted term as a program which meets this specification...