Viktor Kuncak

Milena Vujosevic-Janicic, Mladen Nikolic, Dusan Tosic, Viktor Kuncak: Software verification and graph similarity for automated evaluation of students' assignments. Information & Software Technology 55(6): 1004-1016 (2013)

Swen Jacobs, Viktor Kuncak, Philippe Suter: Reductions for Synthesis Procedures. VMCAI 2013: 88-107

Philipp Rümmer, Hossein Hojjat, Viktor Kuncak: Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report). CoRR abs/1301.4973 (2013)

Philipp Rümmer, Hossein Hojjat, Viktor Kuncak: The Relationship between Craig Interpolation and Recursion-Free Horn Clauses. CoRR abs/1302.4187 (2013)

Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, Philippe Suter: On Integrating Deductive Synthesis and Verification Systems. CoRR abs/1304.5661 (2013)

Rachid Guerraoui, Viktor Kuncak, Giuliano Losa: Abortable Linearizable Modules. Archive of Formal Proofs 2012 (2012)

Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Software synthesis procedures. Commun. ACM 55(2): 103-111 (2012)

Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer: Accelerating Interpolants. ATVA 2012: 187-202

Andrej Spielmann, Viktor Kuncak: Synthesis for Unbounded Bit-Vector Arithmetic. IJCAR 2012: 499-513

Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer: A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM 2012: 247-251

Rachid Guerraoui, Viktor Kuncak, Giuliano Losa: Speculative linearizability. PLDI 2012: 55-66

Ali Sinan Köksal, Viktor Kuncak, Philippe Suter: Constraints as control. POPL 2012: 151-164

Eva Darulova, Viktor Kuncak: Certifying Solutions for Numerical Constraints. RV 2012: 277-291

Thomas Wies, Marco Muñiz, Viktor Kuncak: Deciding Functional Lists with Sublist Sets. VSTTE 2012: 66-81

Milena Vujosevic-Janicic, Viktor Kuncak: Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description. VSTTE 2012: 98-113

Viktor Kuncak, Andrey Rybalchenko (Eds.): Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings. Lecture Notes in Computer Science 7148, Springer 2012, isbn 978-3-642-27939-3

Ali Sinan Köksal, Viktor Kuncak, Philippe Suter: Scala to the Power of Z3: Integrating SMT and Programming. CADE 2011: 400-406

Thomas Wies, Marco Muñiz, Viktor Kuncak: An Efficient Decision Procedure for Imperative Tree Data Structures. CADE 2011: 476-491

Tihomir Gvero, Viktor Kuncak, Ruzica Piskac: Interactive Synthesis of Code Snippets. CAV 2011: 418-423

Eva Darulova, Viktor Kuncak: Trustworthy numerical computation in Scala. OOPSLA 2011: 325-344

Philippe Suter, Ali Sinan Köksal, Viktor Kuncak: Satisfiability Modulo Recursive Programs. SAS 2011: 298-315

Swen Jacobs, Viktor Kuncak: Towards Complete Reasoning about Axiomatic Specifications. VMCAI 2011: 278-293

Philippe Suter, Robin Steiger, Viktor Kuncak: Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI 2011: 403-418

Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak: Predicting and preventing inconsistencies in deployed distributed systems. ACM Trans. Comput. Syst. 28(1) (2010)

Ruzica Piskac, Viktor Kuncak: MUNCH - Automated Reasoner for Sets and Multisets. IJCAR 2010: 149-155

Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Comfusy: A Tool for Complete Functional Synthesis. CAV 2010: 430-433

Viktor Kuncak, Ruzica Piskac, Philippe Suter: Ordered Sets in the Calculus of Data Structures. CSL 2010: 34-48

Jad Hamza, Barbara Jobstmann, Viktor Kuncak: Synthesis for regular specifications over unbounded domains. FMCAD 2010: 101-109

Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, Darko Marinov: Test generation through programming in UDITA. ICSE (1) 2010: 225-234

Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter: Complete functional synthesis. PLDI 2010: 316-329

Philippe Suter, Mirco Dotta, Viktor Kuncak: Decision procedures for algebraic data types with abstractions. POPL 2010: 199-210

Etienne Kneuss, Philippe Suter, Viktor Kuncak: Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. RV 2010: 300-314

Etienne Kneuss, Philippe Suter, Viktor Kuncak: Phantm: PHP analyzer for type mismatch. SIGSOFT FSE 2010: 373-374

Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies: Building a Calculus of Data Structures. VMCAI 2010: 26-44

Kuat Yessenov, Ruzica Piskac, Viktor Kuncak: Collections, Cardinalities, and Relations. VMCAI 2010: 380-395

Thomas Wies, Ruzica Piskac, Viktor Kuncak: Combining Theories with Shared Set Operations. FroCoS 2009: 366-382

Maysam Yabandeh, Nedeljko Vasic, Dejan Kostic, Viktor Kuncak: Simplifying Distributed System Development. HotOS 2009

Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak: CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. NSDI 2009: 229-244

Karen Zee, Viktor Kuncak, Martin C. Rinard: An integrated proof language for imperative programs. PLDI 2009: 338-351

Pierre-Évariste Dagand, Dejan Kostic, Viktor Kuncak: Opis: reliable distributed systems in OCaml. TLDI 2009: 65-78

Ruzica Piskac, Viktor Kuncak: Linear Arithmetic with Stars. CAV 2008: 268-280

Ruzica Piskac, Viktor Kuncak: Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars. CSL 2008: 124-138

Karen Zee, Viktor Kuncak, Martin C. Rinard: Verifying linked data structure implementations. IPDPS 2008: 1-5

Karen Zee, Viktor Kuncak, Martin C. Rinard: Full functional verification of linked data structures. PLDI 2008: 349-361

Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin: Runtime Checking for Separation Logic. VMCAI 2008: 203-217

Ruzica Piskac, Viktor Kuncak: Decision Procedures for Multisets with Cardinality Constraints. VMCAI 2008: 218-232

Viktor Kuncak, Martin C. Rinard: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. CADE 2007: 215-230

Bruno Marnette, Viktor Kuncak, Martin C. Rinard: Polynomial Constraints for Sets with Cardinality Bounds. FoSSaCS 2007: 258-273

Karen Zee, Viktor Kuncak, Michael Taylor, Martin C. Rinard: Runtime Checking for Program Verification. RV 2007: 202-213

Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard: Using First-Order Theorem Provers in the Jahob Data Structure Verification System. VMCAI 2007: 74-88

Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard: Deciding Boolean Algebra with Presburger Arithmetic. J. Autom. Reasoning 36(3): 213-239 (2006)

Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard: Modular Pluggable Analyses for Data Structure Consistency. IEEE Trans. Software Eng. 32(12): 988-1005 (2006)

Viktor Kuncak, Martin C. Rinard: An overview of the Jahob analysis system: project goals and current status. IPDPS 2006

Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard: Field Constraint Analysis. VMCAI 2006: 157-173

Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, Martin C. Rinard: On Verifying Complex Properties using Symbolic Shape Analysis. CoRR abs/cs/0609104 (2006)

Viktor Kuncak, Martin C. Rinard: Decision Procedures for Set-Valued Fields. Electr. Notes Theor. Comput. Sci. 131: 51-62 (2005)

Patrick Lam, Viktor Kuncak, Martin C. Rinard: Crosscutting techniques in program specification and analysis. AOSD 2005: 169-180

Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard: An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. CADE 2005: 260-277

Patrick Lam, Viktor Kuncak, Martin C. Rinard: Hob: A Tool for Verifying Data Structure Consistency. CC 2005: 237-241

Viktor Kuncak, Martin C. Rinard, Bruno Marnette: On Algorithms and Complexity for Sets with Cardinality Constraints. Deduction and Applications 2005

Viktor Kuncak, Daniel Jackson: Relational analysis of algebraic datatypes. ESEC/SIGSOFT FSE 2005: 207-216

Patrick Lam, Viktor Kuncak, Martin C. Rinard: Generalized Typestate Checking for Data Structure Consistency. VMCAI 2005: 430-447

Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard: Implications of a Data Structure Consistency Checking System. VSTTE 2005: 214-226

Bruno Marnette, Viktor Kuncak, Martin C. Rinard: On Algorithms and Complexity for Sets with Cardinality Constraints. CoRR abs/cs/0508123 (2005)

Viktor Kuncak: Binary Search Trees. Archive of Formal Proofs 2004 (2004)

Karen Zee, Viktor Kuncak: File Refinement. Archive of Formal Proofs 2004 (2004)

Patrick Lam, Viktor Kuncak, Martin C. Rinard: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Notices 39(3): 46-55 (2004)

Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard: Verifying a File System Implementation. ICFEM 2004: 373-390

Viktor Kuncak, Martin C. Rinard: Generalized Records and Spatial Conjunction in Role Logic. SAS 2004: 361-376

Viktor Kuncak, Martin C. Rinard: Boolean Algebra of Shape Analysis Constraints. VMCAI 2004: 59-72

Viktor Kuncak, Martin C. Rinard: The First-Order Theory of Sets with Cardinality Constraints is Decidable. CoRR cs.LO/0407045 (2004)

Viktor Kuncak, Martin C. Rinard: On the Theory of Structural Subtyping. CoRR cs.LO/0408015 (2004)

Viktor Kuncak, Martin C. Rinard: On Spatial Conjunction as Second-Order Logic. CoRR cs.LO/0410073 (2004)

Viktor Kuncak, Patrick Lam, Martin C. Rinard: Roles Are Really Great! CoRR cs.PL/0408013 (2004)

Viktor Kuncak, Martin C. Rinard: Typestate Checking and Regular Graph Constraints. CoRR cs.PL/0408014 (2004)

Viktor Kuncak, Martin C. Rinard: On Role Logic. CoRR cs.PL/0408018 (2004)

Viktor Kuncak, Martin C. Rinard: On Generalized Records and Spatial Conjunction in Role Logic. CoRR cs.PL/0408019 (2004)

Viktor Kuncak, K. Rustan M. Leino: On computing the fixpoint of a set of boolean equations. CoRR cs.PL/0408045 (2004)

Viktor Kuncak, Martin C. Rinard: Structural Subtyping of Non-Recursive Types is Decidable. LICS 2003: 96-107

Viktor Kuncak, Martin C. Rinard: Existential Heap Abstraction Entailment Is Undecidable. SAS 2003: 418-438

Mirjana Ivanovic, Viktor Kuncak: Numerical Representations as Purely Functional Data Structures: a New Approach. Informatica, Lith. Acad. Sci. 13(2): 163-176 (2002)

Viktor Kuncak, Patrick Lam, Martin C. Rinard: Role analysis. POPL 2002: 17-32

Silvia Ghilezan, Viktor Kuncak: Confluence of Untyped Lambda Calculus via Simple Types. ICTCS 2001: 38-49

Viktor Kuncak, Patrick Lam, Martin C. Rinard: A Language for Role Specifications. LCPC 2001: 366-382