Fields of expertise
BiographyViktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 41. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification and at Coursera the MOOC "Parallel Programming".
Interpolation and Quantifiers in Ortholattices2024. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024), London, United Kingdom, January 15-16, 2024.
Orthologic with Axioms2024. 51st ACM SIGPLAN Symposium on Principles of Programming Languages, London, United Kingdom, January 17-19, 2024.
Formula Normalizations in Verification2023-06-16. 35th International Conference on Computer Aided Verification, Paris, France.
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata2023.
Decision Procedures for Power StructuresLausanne, EPFL, 2023. DOI : 10.5075/epfl-thesis-10546.
The Complexity of Satisfiability Checking for Symbolic Finite Automata2023-07-03
Combinatory Array Logic with Sums2023-11-11
On Algebraic Array Theories2023
From Verified Scala to STIX File System Embedded Code Using Stainless2022. 14th International Symposium NASA Formal Methods (NFM 2022), Pasadena, CA, USA, May 24–27, 2022. p. 393-410. DOI : 10.1007/978-3-031-06773-0_21.
Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time2022. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2022), Munich, Germany, April 2-7, 2022. p. 196-214. DOI : 10.1007/978-3-030-99527-0_11.
On Verified Scala for STIX File System Embedded Code using Stainless2022-01-12
Optimizing Java on Truffle2022-05-10
BPMN process generation and optimization for readability in the context of telemedecine2022-04-23
Formal Verification of Rust with Stainless2021
Exploiting Errors for Efficiency: A Survey from Circuits to ApplicationsAcm Computing Surveys. 2020-06-01. DOI : 10.1145/3394898.
Zippy LL(1) Parsing with Derivatives2020-01-01. 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ELECTR NETWORK, Jun 15-20, 2020. p. 1036-1051. DOI : 10.1145/3385412.3385992.
Refutation-based synthesis in SMTFormal Methods In System Design. 2019-12-01. DOI : 10.1007/s10703-017-0270-2.
On the complexity of linearizabilityComputing. 2019-09-01. DOI : 10.1007/s00607-018-0596-7.
Monotonic Prefix Consistency in Distributed Systems2018-05-30. 38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Madrid, Spain, June 18-20, 2018. DOI : 10.1007/978-3-319-92612-4_3.
Proactive Synthesis of Recursive Tree-to-String Functions from Examples2017. European Conference on Object-Oriented Programming, Barcelona, Spain, Sun 18 - Fri 23 June 2017.
On verifying causal consistency2017. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, January, 15-21, 2017. p. 626-638. DOI : 10.1145/3009837.3009888.
Termination of Open Higher-Order Programs2017
Programmation Interactive par l'ExemplePublish PhD Defense of Mikaël Mayer, EPFL, Lausanne, Switzerland, September 28, 2017.
The Operational Semantics and Implementation of a Core Dart language2017
Extending Safe C Support In Leon2017
SMT-Based Checking of Predicate-Qualified Types for Scala2016. 7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016. p. 31-40. DOI : 10.1145/2998392.2998398.
A Scala Library for Testing Student Assignments on Concurrent Programming2016. 7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016. p. 1-10. DOI : 10.1145/2998392.2998395.
On Verifying Causal Consistency2016
Automating Verification of Functional Programs with Quantified Invariants2016
Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization2016
On Satisfiability for Quantified Formulas in Instantiation-Based Procedures2016
On recursion-free Horn clauses and Craig interpolationFormal Methods In System Design. 2015. DOI : 10.1007/s10703-014-0219-7.
Synthesizing Java Expressions from Free-Form Queries2015. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015. p. 416-432. DOI : 10.1145/2814270.2814295.
Programming with Enumerable Sets of Structures2015. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015. p. 37-56. DOI : 10.1145/2814270.2814323.
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings2015. 10th International Symposium on Frontiers of Combining Systems (FroCoS), Wroclaw, POLAND, SEP 21-24, 2015. p. 135-150. DOI : 10.1007/978-3-319-24246-0_9.
Developing Verified Software Using Leon2015. 7th NASA Formal Methods Symposium (NFM), Pasadena, CA, APR 27-29, 2015. p. 12-15. DOI : 10.1007/978-3-319-17524-9_2.
Synthesizing Functions from Relations in Leon2015. 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Univ Kent, Canterbury, ENGLAND, SEP 09-11, 2014.
A Decision Procedure for (Co)datatypes in SMT Solvers2015. 25th International Conference on Automated Deduction (CADE), Berlin, GERMANY, AUG 01-07, 2015. p. 197-213. DOI : 10.1007/978-3-319-21401-6_13.
Induction for SMT Solvers2015. 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Mumbai, INDIA, JAN 12-14, 2015. p. 80-98. DOI : 10.1007/978-3-662-46081-8_5.
On Counter-Example Complete Verification for Higher-Order Functions2015
Towards Automating Grammar Equivalence Checking2015
On Deductive Program Repair in Leon2015
Verifying and Synthesizing Software with Recursive Functions2014. 41st International Colloquium on Automata, Languages and Programming. p. 11-25. DOI : 10.1007/978-3-662-43948-7_2.
Sound Compilation of Reals2014. 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)', u'41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). p. 235-248. DOI : 10.1145/2535838.2535874.
On Induction for SMT Solvers2014
On Synthesizing Code from Free-Form Queries2014
On Numerical Error Propagation with Sensitivity2014
Symbolic Resource Bound Inference2014
Contracts for Real-Time, Safety Critical Systems2014
Synthesis Modulo Recursive FunctionsAcm Sigplan Notices. 2013. DOI : 10.1145/2509136.2509555.
Software verification and graph similarity for automated evaluation of students' assignmentsInformation And Software Technology. 2013. DOI : 10.1016/j.infsof.2012.12.005.
Interpolation for Synthesis on Unbounded Domains2013. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, OCT 20-23, 2013. p. 93-96. DOI : 10.1109/FMCAD.2013.6679396.
An overview of the Leon verification system: verification by translation to recursive functions2013. SCALA 2013, Montpellier, France, 2013. DOI : 10.1145/2489837.2489838.
Effect Analysis for Programs with Callbacks2013. Verified Software: Theories, Tools, Experiments, Menlo Park, CA, USA, 2013. p. 48-67. DOI : 10.1007/978-3-642-54108-7_3.
On Repairing Ill-Typed Expressions2013
On Sound Compilation of Reals2013
On Verification by Translation to Recursive Functions2013
On Cafesat: A Modern SAT Solver for Scala2013
On Integrating Deductive Synthesis and Verification Systems2013
Techniques for Program Synthesis2013
On the Generation of Precise Fixed-Point Expressions2013
Interactive Code Generation2013
Abortable Linearizable ModulesArchive of Formal Proofs. 2012.
Symbolic execution of Reo circuits using constraint automataScience Of Computer Programming. 2012. DOI : 10.1016/j.scico.2011.04.001.
Constraints as ControlAcm Sigplan Notices (POPL). 2012. DOI : 10.1145/2103621.2103675.
Software Synthesis ProceduresCommunications of the ACM. 2012. DOI : 10.1145/2076450.2076472.
Constraints as Control2012. 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, Jan 25-27, 2012. p. 151-164. DOI : 10.1145/2103656.2103675.
On Complete Completion using Types and Weights2012
On Reductions for Synthesis Procedures2012
On Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments2012
On Fast Code Completion using Type Inhabitation2012
On Effect Analysis for Programs with Callbacks2012
On the Automatic Computation of Error Bounds for Solutions of Nonlinear Equations2012
On Accelerating Interpolants2012
On Synthesis for Unbounded Bit-vector Arithmetic2012
Leveraging Formal Verification Throughout the Entire Design CycleDesign Verification Club Europe (DVClub 2012), November 21, 2012.
Verification of Imperative Programs in Scala2012
Measuring shape rectangularityElectronics Letters. 2011. DOI : 10.1049/el.2011.0020.
Formal Analysis of SystemC Designs in Process AlgebraFundamenta Informaticae. 2011. DOI : 10.3233/FI-2011-391.
Scala to the Power of Z3: Integrating SMT and Programming2011. 23rd International Conference on Automated Deduction (CADE 23). p. 400-406. DOI : 10.1007/978-3-642-22438-6_30.
Decision Procedures for Automating Termination Proofs2011. 12th International Conference on Verification, Model Checking, and Abstract Interpretation, Austin, TX, Jan 23-25, 2011. p. 371-386. DOI : 10.1007/978-3-642-18275-4_26.
Trustworthy Numerical Computation in Scala2011. ACM Conf. on Object-Oriented Programming, Systems, Languages, and Applications , Portland, Oregon, USA, October 25-27. p. 325-344. DOI : 10.1145/2076021.2048094.
Towards Complete Reasoning about Axiomatic Specifications2011. Verification, Model Checking, and Abstract Interpretation (VMCAI). p. 278-293. DOI : 10.1007/978-3-642-18275-4_20.
Sets with Cardinality Constraints in Satisfiability Modulo Theories2011. Verification, Model Checking, and Abstract Interpretation (VMCAI). p. 403-418. DOI : 10.1007/978-3-642-18275-4_28.
Interactive Synthesis of Code Snippets2011. Computer Aided Verification (CAV), 2011.
Scala to the Power of Z3: Integrating SMT and Programming2011. Computer-Aideded Deduction (CADE).
Satisfiability Modulo Recursive Programs2011. Static Analysis Symposium (SAS), 2011. p. 298-315. DOI : 10.1007/978-3-642-23702-7_23.
PhoneLab: Cloud-Backed Development Environment for Smartphones2011
Code Completion using Quantitative Type Inhabitation2011
On an Efficient Decision Procedure for Imperative Tree Data Structures2011
On the Design and Implementation of SmartFloat and AfﬁneFloat2011
On Interactive Synthesis of Code Snippets2011
Toward Interprocedural Pointer and Effect Analysis for Scala2011
Predicting and Preventing Inconsistencies in Deployed Distributed SystemsACM Transactions on Computer Systems. 2010. DOI : 10.1145/1731060.1731062.
Counterexample-Guided Focus2010. 37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Madrid, SPAIN, Jan 17-23, 2010. p. 249-260. DOI : 10.1145/1706299.1706330.
Automatic Verification of Parametric Specifications with Complex Topologies2010. Integrated Formal Methods 2010, 8th International Conference, Nancy, France, October 11-14, 2010. p. 152–167. DOI : 10.1007/978-3-642-16265-7_12.
Decision Procedures for Algebraic Data Types with Abstractions2010. ACM Symp. Principles of Programming Languages (POPL), 2010. p. 199-210. DOI : 10.1145/1706299.1706325.
Test Generation through Programming in UDITA2010. International Conference on Software Engineering (ICSE), 2010. p. 225–234. DOI : 10.1145/1806799.1806835.
Complete Functional Synthesis2010. ACM Conference on Programming Language Design and Implementation (PLDI), 2010. p. 316–329. DOI : 10.1145/1806596.1806632.
On Satisfiability Modulo Computable Functions2010
On Rigorous Numerical Computation as a Scala Library2010
On Complete Reasoning about Axiomatic Specifications2010
On Sets with Cardinality Constraints in Satisfiability Modulo Theories2010
On Deciding Functional Lists with Sublist Sets2010
On Locality of One-Variable Axioms and Piecewise Combinations2010
On Using Static Analysis to Detect Type Errors in PHP Applications2010
On Decision Procedures for Ordered Collections2010
Well-structured Petri Nets extensions with data2010
Complete Program Synthesis for Linear Arithmetic2010
Static Analysis for the PHP Language2010
Simplifying Distributed System Development2009. 12th Workshop on Hot Topics in Operating Systems.
CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems2009. 6th USENIX Symp. Networked Systems Design and Implementation (NSDI).
On Complete Functional Synthesis2009
On Test Generation through Programming in UDITA2009
On Decision Procedures for Collections, Cardinalities, and Relations2009
On Decision Procedures for Algebraic Data Types with Abstractions2009
On Combining Theories with Shared Set Operations2009
On Set-Driven Combination of Logics and Verifiers2009
Programming with Undo2009
Robust Dynamically Deployed Static Analysis for Java2009
State Exploration of Scala Actor Programs2009
On Delayed Choice Execution for Falsification2008
Constraint Solving for Software Reliability and Text Analysis2008
CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems2008
On Linear Arithmetic with Stars2008
On Static Analysis for Expressive Pattern Matching2008
Non-Clausal Satisfiability Modulo Theories2008
Decision Tree Learning for Drools2008
Runtime Checking for Program Verification Systems2007.
Verifying Complex Properties using Symbolic Shape Analysis2007.
Polynomial Constraints for Sets with Cardinality Bounds2007.
Modular Data Structure Verification2007.
Runtime Checking for Separation Logic2007
Decision Procedures for Multisets with Cardinality Constraints2007
Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete2007
Field Constraint Analysis2006.
An overview of the Jahob analysis system: Project Goals and Current Status2006.
On Verifying Complex Properties using Symbolic Shape Analysis2006
On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System2006
Hob: A Tool for Verifying Data Structure Consistency2005.
Cross-Cutting Techniques in Program Specification and Analysis2005.
Decision Procedures for Set-Valued Fields2005.
Implications of a Data Structure Consistency Checking System2005.
On Field Constraint Analysis2005
On Algorithms and Complexity for Sets with Cardinality Constraints2005
On Relational Analysis of Algebraic Datatypes2005
Combining Theorem proving with Static Analysis for Data Structure Consistency2004.
Generalized Records and Spatial Conjunction in Role Logic2004.
Modular Pluggable Analyses for Data Structure Consistency2004.
Verifying a File System Implementation2004.
On Our Experience with Modular Pluggable Analyses2004
On Spatial Conjunction as Second-Order Logic2004
On Generalized Records and Spatial Conjunction in Role Logic2004
The First-Order Theory of Sets with Cardinality Constraints is Decidable2004
On Decision Procedures for Set-Valued Fields2004
On Verifying a File System Implementation2004
Existential Heap Abstraction Entailment is Undecidable2003.
In-Place Refinement for Effect Checking2003.
On Modular Pluggable Analyses Using Set Interfaces2003
On the Theory of Structural Subtyping2003
On Role Logic2003
On the Boolean Algebra of Shape Analysis Constraints2003
On computing the fixpoint of a set of boolean equations2003
Numerical Representations as Purely Functional Data Structures: A New ApproachINFORMATICA, Institute of Mathematics and Informatics, Vilnius. 2002.
Typestate Checking and Regular Graph Constraints2002
Reducibility method for termination properties of typed lambda terms2001.
Types and confluence in lambda calculus2001. p. 17-21.
Confluence of untyped lambda calculus via simple types2001. 7th Italian Conference on Theoretical Computer Science, ICTCS 2001, Torino, Italy, October 4–6, 2001. p. 38-49. DOI : 10.1007/3-540-45446-2_3.
Object Models, Heaps, and Interpretations2001
Roles are really great!2001
Designing an Algorithm for Role Analysis2001
Numerical Representations as Purely Functional Data Structures2000.
Modular Language Specifications in Haskell2000.
Reducibility Method in Simply Typed Lambda Calculus2000.
Modular Interpreters in Haskell2000
Developing a Multigrid Solver for Standing Wave Equation1996
PLS: Programming Language for Simulations1993. p. 111-146.
Teaching & PhD