BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Kuncak:Viktor

Facilitated 3 volumes:

VMCAI 2012Ed
CAV (1) 2017Ed
CAV (2) 2017Ed

Contributed to:

CAV 20152015
ICSE 20152015
OOPSLA 20152015
VMCAI 20152015
CAV 20142014
ICALP (1) 20142014
POPL 20142014
CAV 20132013
OOPSLA 20132013
Onward! 20132013
PLDI 20132013
SIGMOD 20132013
VMCAI 20132013
FM 20122012
IJCAR 20122012
PLDI 20122012
POPL 20122012
CADE 20112011
CAV 20112011
OOPSLA 20112011
SAS 20112011
VMCAI 20112011
CAV 20102010
CSL 20102010
FSE 20102010
ICSE 20102010
IJCAR 20102010
PLDI 20102010
POPL 20102010
VMCAI 20102010
PLDI 20092009
CAV 20082008
CSL 20082008
PLDI 20082008
VMCAI 20082008
CADE 20072007
FoSSaCS 20072007
VMCAI 20072007
VMCAI 20062006
CADE 20052005
CC 20052005
ESEC/FSE 20052005
VMCAI 20052005
SAS 20042004
VMCAI 20042004
LICS 20032003
SAS 20032003
POPL 20022002
IJCAR 20162016
ECOOP 20172017
OOPSLA 20182018
OOPSLA 20192019
POPL 20172017

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

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.