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  orcid-logo
•
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
Type
conference paper
DOI
10.1007/978-3-642-14295-6_38
Web of Science ID

WOS:000281446200037

Author(s)
Kuncak, Viktor  orcid-logo
Mayer, Mikael  
Piskac, Ruzica  
Suter, Philippe  
Editors
Touili, Tayssir
•
Cook, Byron
•
Jackson, Paul
Date Issued

2010

Publisher

Springer

Published in
Proceedings of the 22nd International Conference on Computer-Aided Verification (CAV)
Series title/Series vol.

Lecture Notes in Computer Science; 6174

Volume

6174

Start page

430

End page

433

Subjects

functional synthesis

•

decision procedure

•

synthesis procedure

•

Scala

Note

Tool Presentation

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
22nd International Conference on Computer Aided Verification

Edinburgh, Scotland, UK

July 15-19, 2010

Available on Infoscience
December 1, 2010
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/61703
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