Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Comfusy: A Tool for Complete Functional Synthesis
 
conference paper

Comfusy: A Tool for Complete Functional Synthesis

Kuncak, Viktor  
•
Mayer, Mikael  
•
Piskac, Ruzica  
Show more
Touili, Tayssir
•
Cook, Byron
Show more
2010
Proceedings of the 22nd International Conference on Computer-Aided Verification (CAV)
22nd International Conference on Computer Aided Verification

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesis over unbounded domains. Comfusy accepts expressions with input and output variables specifying relations on integers and sets. Comfusy symbolically computes the precise domain for the given relation and generates the function from inputs to outputs. The outputs are guaranteed to satisfy the relation whenever the inputs belong to the relation domain. The core of our synthesis algorithm is an extension of quantifier elimination that generates programs to compute witnesses for eliminated variables. We present examples that demonstrate software synthesis using Comfusy and illustrate how synthesis simplifies software development.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

KuncakETAL10Comfusy.pdf

Access type

openaccess

Size

143.73 KB

Format

Adobe PDF

Checksum (MD5)

48750a9d9bfc4454239a462094cc7e48

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés