|
|
|
Viktor Kuncak
|
|
Laboratory for Automated Reasoning and Analysis
|
|
|
|
BIOGRAPHY
|
Viktor Kuncak is interested in automated methods and tools for reasoning about complex properties of software, hardware, and information systems. The overall goal of this research is to increase reliability and productivity of engineering sophisticated computer systems. His most recent work is developing a software verification system for automatically verifying both detailed and high-level properties of software implementations and designs.
Before joining EPFL, Viktor Kuncak was a doctoral student and a research assistant in the Computer Science and Artificial Intelligence Laboratory of the Massachusetts Institute of Technology, Cambridge, USA. In his doctoral thesis, he developed techniques for improving software reliability by automatically proving properties of software that manipulates complex data structures. He has contributed to new algorithms for proving such properties, established their computational complexity, implemented them in the context of program verification systems, and used them to automatically verify properties that were previously beyond the reach of automated verification techniques. He also worked on the foundations of expressive subtyping constraints and applications of interactive theorem proving. He was a summer intern at Software Productivity Tools group in Microsoft Research, Redmond, USA, in 2002 and a visitor at the Max-Planck-Institute for Computer Science, Saarbruecken, Germany, in 2003 and 2005. He served in the program committees of the ACM SIGPLAN 2007 Conference on Programming Language Implementation and Design (PLDI 2007); 13th and 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006, LPAR 2007); and workshops HAV 2007 and ADDCT 2007. He was a reviewer for over 10 conferences and journals.
|
|
MAIN PUBLICATIONS
|
|
|
M. Yabandeh, N. Vasi, D. Kosti, and V. Kuncak.
Simplifying Distributed System Development.
In 12th Workshop on Hot Topics in Operating
Systems, 2009.
[ Details |
Full Text ]
|
|
|
K. Zee, V. Kuncak, and M. Rinard.
An Integrated Proof Language for Imperative Programs.
In ACM Conf. Programming Language Design and
Implementation (PLDI), 2009.
[ Details |
Full Text |
Link ]
|
|
|
M. Yabandeh, N. Knezevic, D. Kostic, and V. Kuncak.
CrystalBall: Predicting and Preventing Inconsistencies in
Deployed Distributed Systems.
In 6th USENIX Symp. Networked Systems Design and
Implementation (NSDI), 2009.
[ Details |
Full Text |
Link ]
|
|
|
P.-� Dagand, D. Kosti, and V. Kuncak.
Opis: Reliable Distributed Systems in OCaml.
In ACM SIGPLAN Workshop on Types in Language Design
and Implementation, 2009.
[ Details |
Full Text |
Link ]
|
|
|
R. Piskac and V. Kuncak.
Fractional Collections with Cardinality Bounds, and Mixed
Integer Linear Arithmetic with Stars.
In Computer Science Logic (CSL), 2008.
[ Details |
Full Text |
Link ]
|
|
|
R. Piskac and V. Kuncak.
Linear Arithmetic with Stars.
In None, LNCS, None, 2008. Springer.
[ Details |
Full Text ]
|
|
|
K. Zee, V. Kuncak, and M. Rinard.
Full Functional Verification of Linked Data Structures.
In ACM Conf. Programming Language Design and
Implementation (PLDI), 2008.
[ Details |
Full Text |
Link ]
|
|
|
R. Piskac and V. Kuncak.
Decision Procedures for Multisets with Cardinality
Constraints.
In 9th International Conference on Verification, Model
Checking, and Abstract Interpretation (VMCAI), LNCS. Springer, 2008.
[ Details |
Full Text |
Link ]
|
|
|
K. Zee, V. Kuncak, and M. Rinard.
Runtime Checking for Program Verification Systems.
In Workshop on Workshop on Runtime Verification
(collocated with AOSD), 2007.
[ Details ]
|
|
|
T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard.
Verifying Complex Properties using Symbolic Shape Analysis.
In Workshop on Heap Abstraction and Verification
(collocated with ETAPS), 2007.
[ Details ]
|
|
|
B. Marnette, V. Kuncak, and M. Rinard.
Polynomial Constraints for Sets with Cardinality Bounds.
In Foundations of Software Science and Computation
Structures (FOSSACS), 2007.
[ Details |
Full Text ]
|
|
|
V. Kuncak and M. Rinard.
Towards Efficient Satisfiability Checking for Boolean
Algebra with Presburger Arithmetic.
In Conference on Automateded Deduction (CADE-21), 2007.
[ Details |
Full Text ]
|
|
|
C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard.
Using First-Order Theorem Provers in the Jahob Data
Structure Verification System.
In Verification, Model Checking and Abstract
Interpretation, 2007.
See http://infoscience.epfl.ch/search.py?recid=110245&ln=en for full
version.
[ Details ]
|
|
|
T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard.
Field Constraint Analysis.
In Proc. Int. Conf. Verification, Model Checking, and
Abstract Interpratation, 2006.
See http://infoscience.epfl.ch/search.py?recid=110237&ln=en for full
version.
[ Details ]
|
|
|
V. Kuncak and M. Rinard.
An overview of the Jahob analysis system: Project Goals and
Current Status.
In NSF Next Generation Software Workshop, 2006.
[ Details |
Full Text ]
|
|
|
P. Lam, V. Kuncak, and M. Rinard.
Hob: A Tool for Verifying Data Structure Consistency.
In 14th International Conference on Compiler
Construction (tool demo), 2005.
[ Details |
Full Text ]
|
|
|
P. Lam, V. Kuncak, and M. Rinard.
Generalized Typestate Checking for Data Structure
Consistency.
In Verification, Model Checking and Abstract
Interpretation, 2005.
[ Details |
Full Text ]
|
|
|
P. Lam, V. Kuncak, and M. Rinard.
Cross-Cutting Techniques in Program Specification and
Analysis.
In 4th International Conference on Aspect-Oriented
Software Development, 2005.
[ Details |
Full Text ]
|
|
|
V. Kuncak and M. Rinard.
Decision Procedures for Set-Valued Fields.
In Workshop on Abstract Interpretation of
Object-Oriented Languages, 2005.
See http://infoscience.epfl.ch/search.py?recid=110224&ln=en for full
version.
[ Details ]
|
|
|
V. Kuncak, H. H. Nguyen, and M. Rinard.
An Algorithm for Deciding BAPA: Boolean Algebra with
Presburger Arithmetic.
In 20th International Conference on Automated
Deduction, CADE-20, 2005.
Superseded by
citeKuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.
[ Details |
Full Text ]
|
|
|
CURRENT WORK
|
|
Automated analysis of rich models of computer systems (See http://lara.epfl.ch for more information.)
|
|
|
Tenure-Track Assistant Professor