Publications by Viktor Kuncak | EPFL Graph Search

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.

A large portion of software is used for numerical computation in mathematics, physics and engineering. Among the aspects that make verification in this domain difficult is the need to quantify numerical errors, such as roundoff errors and errors due to the ...

Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications du ...

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

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

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

We present an approach for using formal methods in embedded systems and its evaluation on a case study. In our approach, the developers describe the system in a restricted subset of the high-level programming language Scala. We then use 1) a verification s ...

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

We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates con ...

We propose a new approach for developing and deploying distributed systems, in which nodes predict distributed consequences of their actions, and use this information to detect and avoid errors. Each node continuously runs a state exploration algorithm on ...

We discuss two extensions to a recently introduced theory of arrays, which are based on considerations coming from the model theory of power structures. First, we discuss how the ordering relation on the index set can be expressed succinctly by referring t ...

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

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

We present an approach for verification of programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write effects. We implement our tool in the Stainless verification system for Scala. A nov ...

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

Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis sy ...

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

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

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

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

Viktor Kuncak

Chat with Graph Search

Certifying Solutions for Numerical Constraints

Runtime Checking for Separation Logic

Game Programming by Demonstration

Proving and Disproving Equivalence of Functional Programming Assignments

Ordered Sets in the Calculus of Data Structures

From Verified Scala to STIX File System Embedded Code Using Stainless

Complete Completion using Types and Weights

Constraints as Control

CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems

Succinct ordering and aggregation constraints in algebraic array theories

NP Satisfiability for Arrays as Powers

Towards Complete Reasoning about Axiomatic Specifications

Generalized Arrays for Stainless Frames

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Verifying and Synthesizing Software with Recursive Functions

Software Synthesis Procedures

An Integrated Proof Language for Imperative Programs

A Verification Toolkit for Numerical Transition Systems

Collections, Cardinalities, and Relations

MUNCH - Automated Reasoner for Sets and Multisets