Publication

On Reductions for Synthesis Procedures

Related publications (35)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Traversal Query Language For Scala.Meta

Eugene Burmako, Eric Beguet

With the rise of metaprogramming in Scala, manipulating ASTs has become a daily job. Yet the standard API provides only low-level mechanisms to transform or to collect information on those data structures. Moreover, those mechanisms often force the program ...

2015

On Counter-Example Complete Verification for Higher-Order Functions

Viktor Kuncak, Etienne Kneuss, Nicolas Charles Yves Voirol

We present a verification procedure for pure higher-order functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counter-examples. The procedure reduces the analysis of higher-orde ...

2015

Spatial joins in main memory: implementation matters!

Darius Sidlauskas

A recent PVLDB paper reports on experimental analyses of ten spatial join techniques in main memory. We build on this comprehensive study to raise awareness of the fact that empirical running time performance findings in main-memory settings are results of ...

2014

Functional synthesis for linear arithmetic and sets

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way—they should succeed for a well-defin ...

Springer Berlin Heidelberg2013

Achieving Efficient Work-Stealing for Data-Parallel Collections

Martin Odersky, Aleksandar Prokopec

In modern programming high-level data-structures are an important foundation for most applications. With the rise of the multi-core era, there is a growing trend of supporting data-parallel collection operations in general purpose programming languages and ...

2013

Synthesis Modulo Recursive Functions

Viktor Kuncak, Etienne Kneuss, Ivan Kuraj, Philippe Paul Henri Suter

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synt ...

2013

Techniques for Program Synthesis

Régis William Blanc

Software synthesis is an attractive field of study that can promise a more safe and productive software development process. However, it is notoriously very difficult and few convincing applications have emerged so far. In this report, we present a series ...

2013

Software Synthesis Procedures

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succ ...

2012

STM in the Small: Trading Generality for Performance in Software Transactional Memory

Aleksandar Dragojevic

Data structures implemented using software transactional memory (STM) have a reputation for being much slower than data structures implemented directly from low-level primitives such as atomic compare-and-swap (CAS). In this paper we present a specialized ...

2012

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

EPFL2011