Publications by Ruzica Piskac | EPFL Graph Search

StriSynth: Synthesis for Live Programming

Abstract—Motivated by applications in automating repetitive file manipulations, we present a tool called StriSynth, which allows end-users to perform transformations over data using examples. Based on provided examples, our tool automatically generates scr ...

2015

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

Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

ACM2013

On Repairing Ill-Typed Expressions

Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

When developing code, a programmer typically knows the approximate structure of the desired expression. However, often the first attempt at writing it down results in an ill-typed code fragment. We propose an approach that automatically repairs code expres ...

2013

On Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that ...

2012

On Fast Code Completion using Type Inhabitation

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that ...

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

Decision Procedures for Automating Termination Proofs

Ruzica Piskac

Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current too ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Code Completion using Quantitative Type Inhabitation

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that ...

2011

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Ruzica Piskac

Graph Chatbot

Chat with Graph Search

StriSynth: Synthesis for Live Programming

Functional synthesis for linear arithmetic and sets

Complete Completion using Types and Weights

On Repairing Ill-Typed Expressions

On Complete Completion using Types and Weights

On Fast Code Completion using Type Inhabitation

Decision Procedures for Program Synthesis and Verification

Decision Procedures for Automating Termination Proofs

Code Completion using Quantitative Type Inhabitation

Ordered Sets in the Calculus of Data Structures

Functional synthesis for linear arithmetic and sets

On Fast Code Completion using Type Inhabitation

Complete Completion using Types and Weights

On Repairing Ill-Typed Expressions

Decision Procedures for Program Synthesis and Verification

Ordered Sets in the Calculus of Data Structures

On Complete Completion using Types and Weights

Code Completion using Quantitative Type Inhabitation

StriSynth: Synthesis for Live Programming

Decision Procedures for Automating Termination Proofs