Travelled to:1 × Austria
1 × China
1 × Czech Republic
1 × Denmark
1 × Estonia
1 × Germany
1 × India
1 × Ireland
1 × Poland
1 × Russia
1 × South Africa
18 × USA
2 × Canada
2 × Portugal
2 × Spain
3 × France
4 × United Kingdom
5 × Italy
Collaborated with:M.C.Rinard R.Piskac P.Suter M.Mayer T.Gvero P.Lam R.Madhavan E.Darulova A.S.Köksal T.Wies E.Kneuss K.Zee I.Kuraj D.Jackson S.Jacobs A.Reynolds A.Spielmann H.H.Nguyen J.Hamza ∅ P.Rümmer H.Hojjat L.Hupel M.Koukoutos R.Guerraoui G.Losa M.Muñiz R.Steiger M.Dotta K.Yessenov W.Chin B.Marnette R.Chugh Nicolas Voirol S.Kulal S.Gulwani M.Deters C.Tinelli C.W.Barrett Y.Klonatos A.Nötzli C.Koch C.Bouillaguet A.Podelski F.Konecný F.Garnier R.Iosif M.Gligoric V.Jagannath S.Khurshid D.Marinov
Talks about:synthesi (10) structur (9) program (9) function (8) data (8) constraint (6) arithmet (5) complet (5) algebra (5) recurs (5)
Person: Viktor Kuncak
DBLP: Kuncak:Viktor
Facilitated 3 volumes:
Ed
EdEdContributed to:
2015
2015
201520152014
2014
201420132013
2013
2013
20132013
2012
201220122012
201120112011
201120112010
2010
201020102010201020102010200920082008200820082007
2007200720062005
2005
2005200520042004
2003200320022016
2017201820192017Wrote 60 papers:
- CAV-2015-KneussKK #deduction #program repair
- Deductive Program Repair (EK, MK, VK), pp. 217–233.
- CAV-2015-ReynoldsDKTB #quantifier #smt #synthesis
- Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.
- ICSE-v2-2015-GveroK #interactive #query #synthesis #using
- Interactive Synthesis Using Free-Form Queries (TG, VK), pp. 689–692.
- OOPSLA-2015-GveroK #java #query
- Synthesizing Java expressions from free-form queries (TG, VK), pp. 416–432.
- OOPSLA-2015-KurajKJ #programming #set
- Programming with enumerable sets of structures (IK, VK, DJ), pp. 37–56.
- OOPSLA-2015-MadhavanMGK #automation #comparison
- Automating grammar comparison (RM, MM, SG, VK), pp. 183–200.
- VMCAI-2015-ReynoldsK #induction #smt
- Induction for SMT Solvers (AR, VK), pp. 80–98.
- CAV-2014-MadhavanK #bound #functional #source code
- Symbolic Resource Bound Inference for Functional Programs (RM, VK), pp. 762–778.
- ICALP-v1-2014-Kuncak #recursion #verification
- Verifying and Synthesizing Software with Recursive Functions — (Invited Contribution) (VK), pp. 11–25.
- POPL-2014-DarulovaK #compilation
- Sound compilation of reals (ED, VK), pp. 235–248.
- CAV-2013-RummerHK #verification
- Disjunctive Interpolants for Horn-Clause Verification (PR, HH, VK), pp. 347–363.
- OOPSLA-2013-KneussKKS #recursion #synthesis
- Synthesis modulo recursive functions (EK, IK, VK, PS), pp. 407–426.
- Onward-2013-MayerK #game studies #programming
- Game programming by demonstration (MM, VK), pp. 75–90.
- PLDI-2013-GveroKKP #using
- Complete completion using types and weights (TG, VK, IK, RP), pp. 27–38.
- SIGMOD-2013-KlonatosNSKK #algorithm #automation #synthesis
- Automatic synthesis of out-of-core algorithms (YK, AN, AS, CK, VK), pp. 133–144.
- VMCAI-2013-JacobsKS #reduction #synthesis
- Reductions for Synthesis Procedures (SJ, VK, PS), pp. 88–107.
- FM-2012-HojjatKGIKR #tool support #verification
- A Verification Toolkit for Numerical Transition Systems — Tool Paper (HH, FK, FG, RI, VK, PR), pp. 247–251.
- IJCAR-2012-SpielmannK #bound #synthesis
- Synthesis for Unbounded Bit-Vector Arithmetic (AS, VK), pp. 499–513.
- PLDI-2012-GuerraouiKL
- Speculative linearizability (RG, VK, GL), pp. 55–66.
- POPL-2012-KoksalKS #constraints
- Constraints as control (ASK, VK, PS), pp. 151–164.
- CADE-2011-KoksalKS #power of #programming #scala #smt
- Scala to the Power of Z3: Integrating SMT and Programming (ASK, VK, PS), pp. 400–406.
- CADE-2011-WiesMK #data type #imperative #performance
- An Efficient Decision Procedure for Imperative Tree Data Structures (TW, MM, VK), pp. 476–491.
- CAV-2011-GveroKP #interactive #synthesis
- Interactive Synthesis of Code Snippets (TG, VK, RP), pp. 418–423.
- OOPSLA-2011-DarulovaK #scala
- Trustworthy numerical computation in Scala (ED, VK), pp. 325–344.
- SAS-2011-SuterKK #recursion #satisfiability #source code
- Satisfiability Modulo Recursive Programs (PS, ASK, VK), pp. 298–315.
- VMCAI-2011-JacobsK #axiom #reasoning #specification #towards
- Towards Complete Reasoning about Axiomatic Specifications (SJ, VK), pp. 278–293.
- VMCAI-2011-SuterSK #constraints #modulo theories #satisfiability #set
- Sets with Cardinality Constraints in Satisfiability Modulo Theories (PS, RS, VK), pp. 403–418.
- CAV-2010-KuncakMPS #functional #named #synthesis
- Comfusy: A Tool for Complete Functional Synthesis (VK, MM, RP, PS), pp. 430–433.
- CSL-2010-KuncakPS #calculus #data type #order #set
- Ordered Sets in the Calculus of Data Structures (VK, RP, PS), pp. 34–48.
- FSE-2010-KneussSK #named #php
- Phantm: PHP analyzer for type mismatch (EK, PS, VK), pp. 373–374.
- ICSE-2010-GligoricGJKKM #generative #programming #testing
- Test generation through programming in UDITA (MG, TG, VJ, SK, VK, DM), pp. 225–234.
- IJCAR-2010-PiskacK #automation #multi #named #set
- MUNCH — Automated Reasoner for Sets and Multisets (RP, VK), pp. 149–155.
- PLDI-2010-KuncakMPS #functional #synthesis
- Complete functional synthesis (VK, MM, RP, PS), pp. 316–329.
- POPL-2010-SuterDK #abstraction #algebra #data type
- Decision procedures for algebraic data types with abstractions (PS, MD, VK), pp. 199–210.
- VMCAI-2010-KuncakPSW #calculus #data type
- Building a Calculus of Data Structures (VK, RP, PS, TW), pp. 26–44.
- VMCAI-2010-YessenovPK
- Collections, Cardinalities, and Relations (KY, RP, VK), pp. 380–395.
- PLDI-2009-ZeeKR #imperative #proving #source code
- An integrated proof language for imperative programs (KZ, VK, MCR), pp. 338–351.
- CAV-2008-PiskacK #linear
- Linear Arithmetic with Stars (RP, VK), pp. 268–280.
- CSL-2008-PiskacK #bound #linear
- Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars (RP, VK), pp. 124–138.
- PLDI-2008-ZeeKR #data type #functional #linked data #open data #verification
- Full functional verification of linked data structures (KZ, VK, MCR), pp. 349–361.
- VMCAI-2008-NguyenKC #logic #runtime
- Runtime Checking for Separation Logic (HHN, VK, WNC), pp. 203–217.
- VMCAI-2008-PiskacK #constraints #multi
- Decision Procedures for Multisets with Cardinality Constraints (RP, VK), pp. 218–232.
- CADE-2007-KuncakR #algebra #performance #satisfiability #towards
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic (VK, MCR), pp. 215–230.
- FoSSaCS-2007-MarnetteKR #bound #constraints #polynomial #set
- Polynomial Constraints for Sets with Cardinality Bounds (BM, VK, MCR), pp. 258–273.
- VMCAI-2007-BouillaguetKWZR #data type #first-order #proving #theorem proving #using #verification
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
- VMCAI-2006-WiesKLPR #analysis #constraints
- Field Constraint Analysis (TW, VK, PL, AP, MCR), pp. 157–173.
- CADE-2005-KuncakNR #algebra #algorithm
- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic (VK, HHN, MCR), pp. 260–277.
- CC-2005-LamKR #consistency #data type #named #verification
- Hob: A Tool for Verifying Data Structure Consistency (PL, VK, MCR), pp. 237–241.
- ESEC-FSE-2005-KuncakJ #algebra #analysis #data type #relational
- Relational analysis of algebraic datatypes (VK, DJ), pp. 207–216.
- VMCAI-2005-LamKR #consistency #data type #type system
- Generalized Typestate Checking for Data Structure Consistency (PL, VK, MCR), pp. 430–447.
- SAS-2004-KuncakR #logic
- Generalized Records and Spatial Conjunction in Role Logic (VK, MCR), pp. 361–376.
- VMCAI-2004-KuncakR #algebra #analysis #constraints
- Boolean Algebra of Shape Analysis Constraints (VK, MCR), pp. 59–72.
- LICS-2003-KuncakR #decidability #recursion #type system
- Structural Subtyping of Non-Recursive Types is Decidable (VK, MCR), pp. 96–107.
- SAS-2003-KuncakR #abstraction #decidability
- Existential Heap Abstraction Entailment Is Undecidable (VK, MCR), pp. 418–438.
- POPL-2002-KuncakLR #analysis
- Role analysis (VK, PL, MCR), pp. 17–32.
- IJCAR-2016-HupelK #higher-order #scala #source code
- Translating Scala Programs to Isabelle/HOL - System Description (LH, VK), pp. 568–577.
- ECOOP-2017-MayerHK #recursion #string #synthesis
- Proactive Synthesis of Recursive Tree-to-String Functions from Examples (MM, JH, VK), p. 30.
- OOPSLA-2018-MayerKC #bidirectional #evaluation
- Bidirectional evaluation with direct manipulation (MM, VK, RC), p. 28.
- OOPSLA-2019-HamzaVK #verification
- System FR: formalized foundations for the stainless verifier (JH, NV, VK), p. 30.
- POPL-2017-MadhavanKK #contract #higher-order #verification
- Contract-based resource verification for higher-order functions with memoization (RM, SK, VK), pp. 330–343.