abstracts | Up ]

Viktor Kuncak: Publications and manuscripts

For details on each manuscript, click on the manuscript [number]. For pdf, click on the manuscript title (footnotes).
[160] Proactive Synthesis of Recursive Tree-to-String Functions from Examples. 31st European Conference on Object-Oriented Programming (ECOOP 2017). 2017. [ bib | DOI | http ]
[159] Towards a Compiler for Reals. ACM Trans. Program. Lang. Syst. (TOPLAS). 2017. [ bib | DOI ]
[158] Contract-Based Resource Verification for Higher-order Functions with Memoization. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2017. [ bib ]
[157] SMT-Based Checking of Predicate-Qualified Types for Scala. Scala Symposium. 2016. [ bib ]
[156] An Update on Deductive Synthesis and Repair in the Leon Tool. 5th Workshop on Synthesis. 2016. [ bib ]
[155] Translating Scala Programs to Isabelle/HOL (System Description). International Joint Conference on Automated Reasoning (IJCAR). 2016. [ps]bib ]
[154] Programming with Enumerable Sets of Structures. OOPSLA. 2015. [ bib ]
[153] Synthesizing Java Expressions from Free-Form Queries. OOPSLA. 2015. [ bib ]
[152] Automating Grammar Comparison. OOPSLA. 2015. [ bib ]
[151] Deductive Program Repair. Computer-Aided Verification (CAV). 2015. [ bib ]
[150] Counterexample Guided Quantifier Instantiation for Synthesis in SMT. Computer-Aided Verification (CAV). 2015. [ bib ]
[149] Counter-Example Complete Verification for Higher-Order Functions. Scala Symposium. 2015. [ bib ]
[148] Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface. Scala Symposium. 2015. [ bib ]
[147] Interactive Synthesis Using Free-Form Queries (Tool Demonstration). International Conference on Software Engineering (ICSE). 2015. [ bib ]
[146] Developing Verified Software Using Leon (Invited Contribution). NASA Formal Methods (NFM). 2015. [ bib ]
[145] Induction for SMT Solvers. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2015. [ bib ]
[144] On Induction for SMT Solvers. EPFL Technical Report EPFL-REPORT-201755. 2014. [ bib ]
[143] On Synthesizing Code from Free-Form Queries. EPFL Technical Report EPFL-REPORT-201606. 2014. [ bib ]
[142] Synthesizing Functions from Relations in Leon (Invited Contribution). Logic-Based Program Synthesis and Transformation (LOPSTR). 2014. [ bib ]
[141] SciFe: Scala Framework for Efficient Enumeration of Data Structures with Invariants. Scala Workshop. 2014. [ bib ]
[140] Checking Data Structure Properties Orders of Magnitude Faster. Runtime Verification (RV). 2014. [ bib ]
[139] Verifying and Synthesizing Software with Recursive Functions (Invited Contribution). 41st International Colloquium on Automata, Languages, and Programming (ICALP). 2014. [ps]bib ]
[138] Symbolic Resource Bound Inference for Functional Programs. Computer Aided Verification (CAV). 2014. [ps]bib ]
[137] On Template-Based Inference of Rich Invariants in Leon. EPFL Technical Report EPFL-REPORT-190578. 2013. [ bib ]
[136] Sound Compilation of Reals. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2014. [ bib ]
[135] Synthesis Modulo Recursive Functions. OOPSLA. 2013. [ps]bib ]
[134] Game Programming by Demonstration. SPLASH Onward!. 2013. [ bib ]
[133] Interpolation for Synthesis on Unbounded Domains. Formal Methods in Computer-Aided Design (FMCAD). 2013. [ bib ]
[132] Synthesis of Fixed-Point Programs. Embedded Software (EMSOFT). 2013. [ps]bib ]
[131] Effect Analysis for Programs with Callbacks. Fifth Working Conference on Verified Software: Theories, Tools and Experiments. 2013. [ bib ]
[130] Classifying and Solving Horn Clauses for Verification. Fifth Working Conference on Verified Software: Theories, Tools and Experiments. 2013. [ bib ]
[129] Executing Specifications using Synthesis and Constraint Solving (Invited Talk). Runtime Verification (RV). 2013. [ps]bib ]
[128] An Overview of the Leon Verification System: Verification by Translation to Recursive Functions. Scala Workshop. 2013. [ps]bib ]
[127] Automatic Synthesis of Out-of-Core Algorithms. SIGMOD. 2013. [ps]bib ]
[126] On Verification by Translation to Recursive Functions. EPFL Technical Report EPFL-REPORT-186233. 2013. [ bib ]
[125] On Integrating Deductive Synthesis and Verification Systems. EPFL Technical Report EPFL-REPORT-186043. 2013. [ bib ]
[124] Disjunctive Interpolants for Horn-Clause Verification. Computer Aided Verification (CAV). 2013. [ bib ]
[123] Complete Completion using Types and Weights. PLDI. 2013. [ bib ]
[122] Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. Information and Software Technology. 2013. [ bib ]
[121] Reductions for Synthesis Procedures. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2013. [ bib | Abstract ]
[120] Certifying Solutions for Numerical Constraints. Runtime Verification (RV). 2012. [ bib | Abstract ]
[119] Accelerating Interpolants. Automated Technology for Verification and Analysis (ATVA). 2012. [ps]bib | Abstract ]
[118] A Verification Toolkit for Numerical Transition Systems (Tool Paper). 16th International Symposium on Formal Methods (FM). 2012. [ bib | Abstract ]
[117] Synthesis for Unbounded Bitvector Arithmetic. International Joint Conference on Automated Reasoning (IJCAR). 2012. [ bib | Abstract ]
[116] Speculative Linearizability. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2012. [ps]bib | Abstract ]
[115] Software Synthesis Procedures. Communications of the ACM. 2012. [ps]bib | Abstract ]
[114] Functional Synthesis for Linear Arithmetic and Sets. Software Tools for Technology Transfer (STTT). 2012. [ bib | Abstract ]
[113] Deciding Functional Lists with Sublist Sets. Verified Software: Theories, Tools and Experiments (VSTTE). 2012. [ps]bib | Abstract ]
[112] Development and Evaluation of LAV: an SMT-Based Error Finding Platform. Verified Software: Theories, Tools and Experiments (VSTTE). 2012. [ps]bib | Abstract ]
[111] Constraints as Control. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2012. [ps]bib | Abstract ]
[110] Trustworthy Numerical Computation in Scala. OOPSLA. 2011. [ps]bib | Abstract ]
[109] Satisfiability Modulo Recursive Programs. Static Analysis Symposium (SAS). 2011. [ps]bib | Abstract ]
[108] An Efficient Decision Procedure for Imperative Tree Data Structures. Computer-Aideded Deduction (CADE). 2011. [ bib | Abstract ]
[107] Scala to the Power of Z3: Integrating SMT and Programming. Computer-Aideded Deduction (CADE) Tool Demo. 2011. [ bib | Abstract ]
[106] Interactive Synthesis of Code Snippets. Computer Aided Verification (CAV) Tool Demo. 2011. [ bib | Abstract ]
[105] Sets with Cardinality Constraints in Satisfiability Modulo Theories. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2011. [ps]bib | Abstract ]
[104] Towards Complete Reasoning about Axiomatic Specifications. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2011. [ps]bib | Abstract ]
[103] On Satisfiability Modulo Computable Functions. EPFL Technical Report EPFL-REPORT. 2010. [ bib ]
[102] On Rigorous Numerical Computation as a Scala Library. EPFL Technical Report EPFL-REPORT-158754. 2010. [ bib ]
[101] Phantm: PHP Analyzer for Type Mismatch (Research Demonstration). ACM SIGSOFT Conference on Foundations of Software Engineering (FSE). 2010. [ps]bib | Abstract ]
[100] Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. International Conference on Runtime Verification. 2010. [ps]bib | Abstract ]
[99] Synthesis for Regular Specifications over Unbounded Domains. FMCAD. 2010. [ps]bib | Abstract ]
[98] Ordered Sets in the Calculus of Data Structures (Invited Paper). CSL. 2010. [ps]bib | Abstract ]
[97] On Deciding Functional Lists with Sublist Sets. EPFL Technical Report EPFL-REPORT-148361. 2010. [ps]bib | Abstract ]
[96] On Locality of One-Variable Axioms and Piecewise Combinations. EPFL Technical Report EPFL-REPORT-148180. 2010. [ps]bib | Abstract ]
[95] MUNCH - Automated Reasoner for Sets and Multisets (System Description). IJCAR. 2010. [ps]bib | Abstract ]
[94] Comfusy: Complete Functional Synthesis (Tool Presentation). CAV. 2010. [ps]bib | Abstract ]
[93] Complete Functional Synthesis. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2010. [ps]bib | Abstract ]
[92] On Decision Procedures for Ordered Collections. EPFL Technical Report LARA-REPORT-2010-001. 2010. [ps]bib | Abstract ]
[91] Test Generation through Programming in UDITA. International Conference on Software Engineering (ICSE). 2010. [ps]bib | http | Abstract ]
[90] Predicting and Preventing Inconsistencies in Deployed Distributed Systems. ACM Transactions on Computer Systems. 2010. [ps]bib | Abstract ]
[89] Building a Calculus of Data Structures (invited paper). Verification, Model Checking, and Abstract Interpretation (VMCAI). 2010. [ps]bib | Abstract ]
[88] Collections, Cardinalities, and Relations. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2010. [ps]bib | Abstract ]
[87] Decision Procedures for Algebraic Data Types with Abstractions. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2010. [ps]bib | Abstract ]
[86] On Complete Functional Synthesis. EPFL Technical Report LARA-REPORT-2009-006. 2009. [ps]bib ]
[85] On Test Generation through Programming in UDITA. EPFL, IC Technical Report LARA-REPORT-2009-05. 2009. [ps]bib | http | Abstract ]
[84] On Decision Procedures for Collections, Cardinalities, and Relations. EPFL Technical Report LARA-REPORT-2009-004. 2009. [ps]bib | Abstract ]
[83] On Decision Procedures for Algebraic Data Types with Abstractions. EPFL Technical Report LARA-REPORT-2009-003. 2009. [ps]bib | Abstract ]
[82] Combining Theories with Shared Set Operations. FroCoS: Frontiers in Combining Systems. 2009. [ps]bib | Abstract ]
[81] On Combining Theories with Shared Set Operations. EPFL Technical Report LARA-REPORT-2009-002. 2009. [ bib ]
[80] Simplifying Distributed System Development. 12th Workshop on Hot Topics in Operating Systems. 2009. [ps]bib | Abstract ]
[79] An Integrated Proof Language for Imperative Programs. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2009. [ps]bib | Abstract ]
[78] On Set-Driven Combination of Logics and Verifiers. EPFL Technical Report LARA-REPORT-2009-001. 2009. [ bib | Abstract ]
[77] Simplifying Distributed System Development. EPFL Technical Report NSL-REPORT-2009-001. 2009. [ bib | Abstract ]
[76] CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. 6th USENIX Symp. Networked Systems Design and Implementation (NSDI '09). 2009. [ps]bib | .html | Abstract ]
[75] Opis: Reliable Distributed Systems in OCaml. ACM SIGPLAN TLDI. 2009. [ bib | Abstract ]
[74] On Delayed Choice Execution for Falsification. EPFL, IC Technical Report LARA-REPORT-2008-08. 2008. [ bib ]
[73] Constraint Solving for Software Reliability and Text Analysis (Research Plan). EPFL Technical Report LARA-REPORT-2008-007. 2008. [ bib | Abstract ]
[72] Opis: Reliable Distributed Systems in OCaml. EPFL-IC-NSL Technical Report NSL-REPORT-2008-001. 2008. [ bib | Abstract ]
[71] CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. EPFL-IC-LARA Technical Report LARA-REPORT-2008-006. 2008. [ bib | Abstract ]
[70] Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars. Computer Science Logic (CSL). 2008. [ps]bib | Abstract ]
[69] Linear Arithmetic with Stars. Computed-Aided Verification (CAV). 2008. [ps]bib | Abstract ]
[68] Full Functional Verification of Linked Data Structures. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2008. [ps]bib | Abstract ]
[67] On Linear Arithmetic with Stars. EPFL Technical Report LARA-REPORT-2008-005. 2008. [ps]bib | Abstract ]
[66] On Static Analysis for Expressive Pattern Matching. EPFL Technical Report LARA-REPORT-2008-004. 2008. [ps]bib | Abstract ]
[65] Decision Procedures for Multisets with Cardinality Constraints. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 2008. [ps]bib | Abstract ]
[64] Runtime Checking for Separation Logic. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 2008. [ bib | Abstract ]
[63] Decision Procedures for Multisets with Cardinality Constraints. EPFL Technical Report LARA-REPORT-2007-002. 2007. [ bib | Abstract ]
[62] Runtime Checking for Separation Logic. EPFL Technical Report LARA-REPORT-2007-003. 2007. [ bib | Abstract ]
[61] Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. Conference on Automateded Deduction (CADE-21). 2007. [ps]bib | Abstract ]
[60] Polynomial Constraints for Sets with Cardinality Bounds. Foundations of Software Science and Computation Structures (FOSSACS). 2007. [ps]bib | Abstract ]
[59] Verifying Complex Properties using Symbolic Shape Analysis. Workshop on Heap Abstraction and Verification (collocated with ETAPS). 2007. [ps]bib ]
[58] Runtime Checking for Program Verification. Workshop on Runtime Verification. 2007. [ bib | Abstract ]
[57] Modular Data Structure Verification. PhD Thesis, EECS Department, Massachusetts Institute of Technology. 2007. [ps]bib | http | Abstract ]
[56] Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete. MIT CSAIL Technical Report MIT-CSAIL-TR-2007-001. 2007. [ps]bib | http | Abstract ]
[55] Using First-Order Theorem Provers in the Jahob Data Structure Verification System. Verification, Model Checking and Abstract Interpretation. 2007. [ps]bib | Abstract ]
[54] On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System. MIT Technical Report MIT-CSAIL-TR-2006-072. 2006. [ps]bib | http | Abstract ]
[53] Modular Pluggable Analyses for Data Structure Consistency. IEEE Transactions on Software Engineering (TSE). 2006. [ps]bib | http | Abstract ]
[52] On Verifying Complex Properties using Symbolic Shape Analysis. Max-Planck Institute for Computer Science Technical Report MPI-I-2006-2-1. 2006. [ bib | http | Abstract ]
[51] Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning. 2006. [ps]bib | http | Abstract ]
[50] An overview of the Jahob analysis system: Project Goals and Current Status. NSF Next Generation Software Workshop. 2006. [ps]bib | Abstract ]
[49] Field Constraint Analysis. Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation. 2006. [ps]bib | Abstract ]
[48] On Field Constraint Analysis. MIT CSAIL Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010. 2005. [ps]bib | Abstract ]
[47] Implications of a Data Structure Consistency Checking System. International conference on Verified Software: Theories, Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference). 2005. [ps]bib | Abstract ]
[46] Relational Analysis of Algebraic Datatypes. 10th European Soft. Eng. Conf. (ESEC) and 13th Symp. Foundations of Software Engineering (FSE). 2005. [ps]bib | Abstract ]
[45] On Algorithms and Complexity for Sets with Cardinality Constraints. MIT CSAIL Technical Report 2005. [ps]bib | http | Abstract ]
[44] An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. 20th International Conference on Automated Deduction, CADE-20. 2005. [ps]bib | Abstract ]
[43] On Relational Analysis of Algebraic Datatypes. MIT Technical Report 985. 2005. [ps]bib | Abstract ]
[42] Hob: A Tool for Verifying Data Structure Consistency. 14th International Conference on Compiler Construction (tool demo). 2005. [ps]bib | Abstract ]
[41] Cross-Cutting Techniques in Program Specification and Analysis. 4th International Conference on Aspect-Oriented Software Development. 2005. [ps]bib | Abstract ]
[40] Decision Procedures for Set-Valued Fields. Electr. Notes Theor. Comput. Sci.; Proc. Abstract Interpretation of Object-Oriented Languages. 2005. [ps]bib | Abstract ]
[39] Generalized Typestate Checking for Data Structure Consistency. Verification, Model Checking and Abstract Interpretation. 2005. [ps]bib | Abstract ]
[38] File Refinement. The Archive of Formal Proofs. 2004. [ bib | http ]
[37] Binary Search Trees. The Archive of Formal Proofs. 2004. [ bib | http ]
[36] Modular Pluggable Analyses for Data Structure Consistency. Monterey Workshop on Software Engineering Tools: Compatibility and Integration. 2004. [ bib ]
[35] On Decision Procedures for Set-Valued Fields. MIT CSAIL Technical Report 975. 2004. [ps]bib | Abstract ]
[34] Combining Theorem proving with Static Analysis for Data Structure Consistency. International Workshop on Software Verification and Validation. 2004. [ps]bib | Abstract ]
[33] On Spatial Conjunction as Second-Order Logic. MIT CSAIL Technical Report 970. 2004. [ps]bib | http | Abstract ]
[32] On Our Experience with Modular Pluggable Analyses. MIT CSAIL Technical Report 965. 2004. [ps]bib | Abstract ]
[31] The First-Order Theory of Sets with Cardinality Constraints is Decidable. MIT CSAIL Technical Report 958. 2004. [ps]bib | http | Abstract ]
[30] Verifying a File System Implementation. Sixth International Conference on Formal Engineering Methods. 2004. [ps]bib | Abstract ]
[29] Generalized Records and Spatial Conjunction in Role Logic. International Static Analysis Symposium. 2004. [ps]bib | Abstract ]
[28] On Generalized Records and Spatial Conjunction in Role Logic. MIT CSAIL Technical Report 942. 2004. [ps]bib | http | Abstract ]
[27] On Verifying a File System Implementation. MIT CSAIL Technical Report 946. 2004. [ps]bib | Abstract ]
[26] Boolean Algebra of Shape Analysis Constraints. Verification, Model Checking and Abstract Interpretation. 2004. [ps]bib | Abstract ]
[25] On computing the fixpoint of a set of boolean equations. Microsoft Research Technical Report MSR-TR-2003-08. 2003. [ps]bib | http | Abstract ]
[24] On Modular Pluggable Analyses Using Set Interfaces. MIT CSAIL Technical Report 933. 2003. [ps]bib | Abstract ]
[23] Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses. SIGPLAN Notices. 2004. [ps]bib | Abstract ]
[22] On Role Logic. MIT CSAIL Technical Report 925. 2003. [ps]bib | http | Abstract ]
[21] On the Boolean Algebra of Shape Analysis Constraints. MIT CSAIL Technical Report 2003. [ps]bib | Abstract ]
[20] Structural Subtyping of Non-Recursive Types is Decidable. Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS). 2003. [ps]bib | Abstract ]
[19] Existential Heap Abstraction Entailment is Undecidable. 10th Annual International Static Analysis Symposium. 2003. [ps]bib | Abstract ]
[18] In-Place Refinement for Effect Checking. Workshop on Automated Verification of Infinite-State Systems. 2003. [ps]bib | Abstract ]
[17] On the Theory of Structural Subtyping. MIT LCS Technical Report 879. 2003. [ps]bib | http | Abstract ]
[16] Typestate Checking and Regular Graph Constraints. MIT LCS Technical Report 863. 2002. [ps]bib | http | Abstract ]
[15] Role Analysis. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2002. [ps]bib | Abstract ]
[14] Designing an Algorithm for Role Analysis. Master's Thesis, MIT LCS. 2001. [ps]bib | Abstract ]
[13] Roles are really great!. MIT LCS Technical Report 822. 2001. [ps]bib | Abstract ]
[12] A Language for Role Specifications. Workshop on Languages and Compilers for Parallel Computing. 2001. [ps]bib | Abstract ]
[11] Object Models, Heaps, and Interpretations. MIT LCS Technical Report 816. 2001. [ps]bib | Abstract ]
[10] Numerical Representations as Purely Functional Data Structures: A New Approach. INFORMATICA, Institute of Mathematics and Informatics, Vilnius. 2002. [ bib ]
[9] Types and confluence in lambda calculus. 3rd Panhellenic Logic Symposium. 2001. [ bib ]
[8] Confluence of untyped lambda calculus via simple types. Proceedings of the 7th Italian Conference on Theoretical Computer Science, ICTCS 2001. 2001. [ bib ]
[7] Reducibility method for termination properties of typed lambda terms. Fifth International Workshop on Termination. 2001. [ bib ]
[6] Modular Language Specifications in Haskell. Theoretical Aspects of Computer Science with practical application. 2000. [ps]bib | Abstract ]
[5] Modular Interpreters in Haskell. B.Sc. Thesis, University of Novi Sad. 2000. [ps]bib ]
[4] Numerical Representations as Purely Functional Data Structures. XIV Conference on Applied Mathematics PRIM, Palić. 2000. [ bib ]
[3] Reducibility Method in Simply Typed Lambda Calculus. XIV Conference on Applied Mathematics PRIM, Palić. 2000. [ bib ]
[2] Developing a Multigrid Solver for Standing Wave Equation. Proceedings of the 28th Dr. Bessie F. Lawrence International Summer Science Institute Participants, Weizmann Institute of Science. 1996. [ps]bib | Abstract ]
[1] PLS: Programming Language for Simulations. Proceedings of the Petnica Science Center Seminar '93. 1993. [ bib | Abstract ]