Person

Viktor Kuncak

Related publications (131)

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.

On the Generation of Precise Fixed-Point Expressions

Viktor Kuncak, Eva Darulova, Indranil Saha

Several problems in the implementations of control systems, signal-processing systems, and scientific computing systems reduce to compiling a polynomial expression over the reals into an imperative program using fixed-point arithmetic. Fixed-point arithmet ...

2013

On Verification by Translation to Recursive Functions

Viktor Kuncak, Etienne Kneuss, Régis William Blanc, Philippe Paul Henri Suter

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

On Sound Compilation of Reals

Viktor Kuncak, Eva Darulova

Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming model where the user writes a program in a real-valued implementation and sp ...

2013

Synthesis of Fixed-Point Programs

Viktor Kuncak, Eva Darulova, Indranil Saha

2013

Software verification and graph similarity for automated evaluation of students' assignments

Viktor Kuncak

Context: The number of students enrolled in universities at standard and on-line programming courses is rapidly increasing. This calls for automated evaluation of students assignments. Objective: We aim to develop methods and tools for objective and reljab ...

Elsevier2013

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 ...

Springer Berlin Heidelberg2013

An overview of the Leon verification system: verification by translation to recursive functions

Viktor Kuncak, Etienne Kneuss, Régis William Blanc, Philippe Paul Henri Suter

2013

Interpolation for Synthesis on Unbounded Domains

Viktor Kuncak, Régis William Blanc

Synthesis procedures compile relational specifications into functions. In addition to bounded domains, synthesis procedures are applicable to domains such as mathematical integers, where the domain and range of relations and synthesized code is unbounded. ...

Ieee2013

Game Programming by Demonstration

Viktor Kuncak, Mikaël Mayer

The increasing adoption of smartphones and tablets has provided tens of millions of users with substantial resources for computation, communication and sensing. The availability of these resources has a huge potential to positively transform our society an ...

2013

On Accelerating Interpolants

Viktor Kuncak, Hossein Hojjat

We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), a new algorithm for verifying infinite-state transition systems. CEGAAR combines interpolation-based predicate discovery in counterexample guided predicate abstraction with accel ...

2012