Recherche

Afficher tous les résultats pour

Accueil

Personne

Viktor Kuncak

À propos
Confidentialité
Mentions légales

Graph Chatbot

Publications associées (81)

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

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

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

Test Generation through Programming in UDITA

Viktor Kuncak, Milos Gligoric, Tihomir Gvero

2010

Decision Procedures for Algebraic Data Types with Abstractions

Mirco Dotta, Philippe Paul Henri Suter, Viktor Kuncak

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...

2010

Predicting and Preventing Inconsistencies in Deployed Distributed Systems

Dejan Kostic, Nikola Knezevic, Viktor Kuncak, Maysam Yabandeh

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

Association for Computing Machinery2010

Ordered Sets in the Calculus of Data Structures

Philippe Paul Henri Suter, Viktor Kuncak, 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

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

2010

Opis: Reliable Distributed Systems in OCaml

Dejan Kostic, Viktor Kuncak, Pierre-Evariste Dagand

Concurrency and distribution pose algorithmic and implementation challenges in developing reliable distributed systems, making the field an excellent testbed for evaluating programming language and verification paradigms. Several specialized domain-specifi ...

2009

CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems

Dejan Kostic, Nikola Knezevic, Viktor Kuncak, Maysam Yabandeh

2009

Simplifying Distributed System Development

Dejan Kostic, Viktor Kuncak, Maysam Yabandeh, Nedeljko Vasic

2009

Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...

Springer2009

Simplifying Distributed System Development

Dejan Kostic, Viktor Kuncak, Maysam Yabandeh, Nedeljko Vasic

Distributed systems are difficult to design and develop. The difficulties arise both in basic safety correctness properties, and in achieving high performance. As a result of this complexity, the implementation of a distributed system often contains the ba ...

2009

An Integrated Proof Language for Imperative Programs

Viktor Kuncak

2009

CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems

Dejan Kostic, Nikola Knezevic, Viktor Kuncak, Maysam Yabandeh

2009

Opis: Reliable Distributed Systems in OCaml

Dejan Kostic, Viktor Kuncak, Pierre-Evariste Dagand

2009

Constraint Solving for Software Reliability and Text Analysis

Viktor Kuncak

We will develop and implement new algorithms for constraint solving and apply them to construct two classes of tools: 1) bug finding and verification tools building on tools such as Java PathFinder and Jahob; 2) tools for deep semantic analysis of texts co ...

2008

Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unk ...

2008

Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We consider an extension of integer linear arithmetic with a “star” operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We show that the satisfiability problem for this extended language remains in NP (and th ...

Springer2008

Runtime Checking for Separation Logic

Viktor Kuncak

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

Springer2008

Decision Procedures for Multisets with Cardinality Constraints

Viktor Kuncak, Ruzica Piskac

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...

Springer2008

Page 4 sur 5