Publications de Viktor Kuncak | EPFL Graph Search

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

On Effect Analysis for Programs with Callbacks

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

We introduce a precise interprocedural effect analysis for programs with mutable state, dynamic object allocation, and dynamic dispatch. Our analysis is precise even in the presence of dynamic dispatch where the context-insensitive estimate on the number o ...

2012

On Fast Code Completion using Type Inhabitation

Viktor Kuncak, Tihomir Gvero, Ivan Kuraj, Ruzica Piskac

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 Reductions for Synthesis Procedures

Viktor Kuncak, Philippe Paul Henri Suter, Swen Jacobs

A synthesis procedure acts as a compiler for declarative specifications. It accepts a formula describing a relation between inputs and outputs, and generates a function implementing this relation. This paper presents synthesis procedures for data structure ...

2012

Abortable Linearizable Modules

Rachid Guerraoui, Viktor Kuncak, Giuliano Losa

We define the Abortable Linearizable Module automaton (ALM for short) and prove its key composition property using the IOA theory of HOLCF. The ALM is at the heart of the Speculative Linearizability framework. This framework simplifies devising correct spe ...

2012

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

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

Speculative Linearizability

Rachid Guerraoui, Viktor Kuncak, Giuliano Losa

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the a ...

2011

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

Towards Complete Reasoning about Axiomatic Specifications

Viktor Kuncak, Swen Jacobs

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...

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

Viktor Kuncak

Graph Chatbot

Chattez avec Graph Search

On Effect Analysis for Programs with Callbacks

On Fast Code Completion using Type Inhabitation

On Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments

On Reductions for Synthesis Procedures

Abortable Linearizable Modules

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Speculative Linearizability

Satisfiability Modulo Recursive Programs

Towards Complete Reasoning about Axiomatic Specifications

PhoneLab: Cloud-Backed Development Environment for Smartphones

On Reductions for Synthesis Procedures

On Fast Code Completion using Type Inhabitation

Abortable Linearizable Modules

On Effect Analysis for Programs with Callbacks

On Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments

Satisfiability Modulo Recursive Programs

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Towards Complete Reasoning about Axiomatic Specifications

Speculative Linearizability

PhoneLab: Cloud-Backed Development Environment for Smartphones