Viktor Kuncak: Publications and manuscripts

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