Publications de Ruzica Piskac | EPFL Graph Search

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

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

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

Interactive Synthesis of Code Snippets

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero

2011

MUNCH - Automated Reasoner for Sets and Multisets

Viktor Kuncak, Ruzica Piskac

This system description provides an overview of the MUNCH reasoner for sets and multisets. MUNCH takes as the input a formula in a logic that supports expressions about sets, multisets, and integers. Constraints over collections and integers are connected ...

Springer2010

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

Collections, Cardinalities, and Relations

Viktor Kuncak, Ruzica Piskac

Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to co ...

2010

Comfusy: A Tool for Complete Functional Synthesis

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. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesi ...

Springer2010

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

Complete Functional Synthesis

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

2010