| 2026 | CAV | Formally Verified Linear-Time Invertible Lexing. | Samuel Chassot, Viktor Kuncak |
| 2025 | CADE | Interoperability of Proof Systems with SC-TPTP. | Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak |
| 2025 | EMNLP | RLMEval: Evaluating Research-Level Neural Theorem Proving. | Auguste Poiroux, Antoine Bosselut, Viktor Kuncak |
| 2025 | EMNLP | Reliable Evaluation and Benchmarks for Statement Autoformalization. | Auguste Poiroux, Gail Weiss, Viktor Kuncak, Antoine Bosselut |
| 2025 | ESOP | Formal Autograding in a Classroom. | Dragana Milovancevic, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, Viktor Kuncak |
| 2025 | VMCAI | Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study. | Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kuncak |
| 2024 | IJCAR | Verifying a Realistic Mutable Hash Table - Case Study (Short Paper). | Samuel Chassot, Viktor Kuncak |
| 2024 | IFM | Proving Termination via Measure Transfer in Equivalence Checking. | Dragana Milovancevic, Carsten Fuhs, Mario Bucev, Viktor Kuncak |
| 2024 | ITP | Mechanized HOL Reasoning in Set Theory. | Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak |
| 2024 | VMCAI | Interpolation and Quantifiers in Ortholattices. | Simon Guilloud, Sankalp Gambhir, Viktor Kuncak |
| 2023 | CAV | Formula Normalizations in Verification. | Simon Guilloud, Mario Bucev, Dragana Milovancevic, Viktor Kuncak |
| 2023 | ITP | LISA - A Modern Proof System. | Simon Guilloud, Sankalp Gambhir, Viktor Kuncak |
| 2023 | LPAR | On the Complexity of Convex and Reverse Convex Prequadratic Constraints. | Rodrigo Raya, Jad Hamza, Viktor Kuncak |
| 2022 | FMCAD | Formally Verified Quite OK Image Format. | Mario Bucev, Viktor Kuncak |
| 2022 | TACAS | Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. | Simon Guilloud, Viktor Kuncak |
| 2022 | VMCAI | NP Satisfiability for Arrays as Powers. | Rodrigo Raya, Viktor Kuncak |
| 2022 | VMCAI | Generalized Arrays for Stainless Frames. | Georg Stefan Schmid, Viktor Kuncak |
| 2021 | FMCAD | Stainless Verification System Tutorial. | Viktor Kuncak, Jad Hamza |
| 2020 | PLDI | Zippy LL(1) parsing with derivatives. | Romain Edelmann, Jad Hamza, Viktor Kuncak |
| 2019 | VMCAI | Minimal Synthesis of String to String Functions from Examples. | Jad Hamza, Viktor Kuncak |
| 2017 | ECOOP | Proactive Synthesis of Recursive Tree-to-String Functions from Examples. | Mikal Mayer, Jad Hamza, Viktor Kuncak |
| 2017 | POPL | Contract-based resource verification for higher-order functions with memoization. | Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak |
| 2016 | CADE | Translating Scala Programs to Isabelle/HOL - System Description. | Lars Hupel, Viktor Kuncak |
| 2015 | CAV | Deductive Program Repair. | Etienne Kneuss, Manos Koukoutos, Viktor Kuncak |
| 2015 | CAV | Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. | Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett |
| 2015 | ICSE | Interactive Synthesis Using Free-Form Queries. | Tihomir Gvero, Viktor Kuncak |
| 2015 | OOPSLA | Synthesizing Java expressions from free-form queries. | Tihomir Gvero, Viktor Kuncak |
| 2015 | OOPSLA | Programming with enumerable sets of structures. | Ivan Kuraj, Viktor Kuncak, Daniel Jackson |
| 2015 | OOPSLA | Automating grammar comparison. | Ravichandhran Madhavan, Mikal Mayer, Sumit Gulwani, Viktor Kuncak |
| 2015 | PLDI | Sound reasoning about integral data types with a reusable SMT solver interface. | Rgis Blanc, Viktor Kuncak |
| 2015 | PLDI | Counter-example complete verification for higher-order functions. | Nicolas Voirol, Etienne Kneuss, Viktor Kuncak |
| 2015 | VMCAI | Induction for SMT Solvers. | Andrew Reynolds, Viktor Kuncak |
| 2014 | CAV | Symbolic Resource Bound Inference for Functional Programs. | Ravichandhran Madhavan, Viktor Kuncak |
| 2014 | ECOOP | SciFe: Scala framework for efficient enumeration of data structures with invariants. | Ivan Kuraj, Viktor Kuncak |
| 2014 | ICALP | Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution). | Viktor Kuncak |
| 2014 | POPL | Sound compilation of reals. | Eva Darulova, Viktor Kuncak |
| 2014 | RV | Checking Data Structure Properties Orders of Magnitude Faster. | Emmanouil Koukoutos, Viktor Kuncak |
| 2013 | CAV | Disjunctive Interpolants for Horn-Clause Verification. | Philipp Rmmer, Hossein Hojjat, Viktor Kuncak |
| 2013 | ECOOP | An overview of the Leon verification system: verification by translation to recursive functions. | Rgis Blanc, Viktor Kuncak, Etienne Kneuss, Philippe Suter |
| 2013 | EMSOFT | Synthesis of fixed-point programs. | Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha |
| 2013 | FMCAD | Interpolation for synthesis on unbounded domains. | Viktor Kuncak, Rgis Blanc |
| 2013 | OOPSLA | Synthesis modulo recursive functions. | Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, Philippe Suter |
| 2013 | OOPSLA | Game programming by demonstration. | Mikal Mayer, Viktor Kuncak |
| 2013 | PLDI | Complete completion using types and weights. | Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac |
| 2013 | SIGMOD | Automatic synthesis of out-of-core algorithms. | Yannis Klonatos, Andres Ntzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak |
| 2013 | RV | Executing Specifications Using Synthesis and Constraint Solving. | Viktor Kuncak, Etienne Kneuss, Philippe Suter |
| 2013 | VMCAI | Reductions for Synthesis Procedures. | Swen Jacobs, Viktor Kuncak, Philippe Suter |
| 2012 | ATVA | Accelerating Interpolants. | Hossein Hojjat, Radu Iosif, Filip Konecn, Viktor Kuncak, Philipp Rmmer |
| 2012 | CADE | Synthesis for Unbounded Bit-Vector Arithmetic. | Andrej Spielmann, Viktor Kuncak |
| 2012 | FM | A Verification Toolkit for Numerical Transition Systems - Tool Paper. | Hossein Hojjat, Filip Konecn, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rmmer |
| 2012 | PLDI | Speculative linearizability. | Rachid Guerraoui, Viktor Kuncak, Giuliano Losa |
| 2012 | POPL | Constraints as control. | Ali Sinan Kksal, Viktor Kuncak, Philippe Suter |
| 2012 | RV | Certifying Solutions for Numerical Constraints. | Eva Darulova, Viktor Kuncak |
| 2011 | CADE | Scala to the Power of Z3: Integrating SMT and Programming. | Ali Sinan Kksal, Viktor Kuncak, Philippe Suter |
| 2011 | CADE | An Efficient Decision Procedure for Imperative Tree Data Structures. | Thomas Wies, Marco Muiz, Viktor Kuncak |
| 2011 | CAV | Interactive Synthesis of Code Snippets. | Tihomir Gvero, Viktor Kuncak, Ruzica Piskac |
| 2011 | OOPSLA | Trustworthy numerical computation in Scala. | Eva Darulova, Viktor Kuncak |
| 2011 | SAS | Satisfiability Modulo Recursive Programs. | Philippe Suter, Ali Sinan Kksal, Viktor Kuncak |
| 2011 | VMCAI | Towards Complete Reasoning about Axiomatic Specifications. | Swen Jacobs, Viktor Kuncak |
| 2011 | VMCAI | Sets with Cardinality Constraints in Satisfiability Modulo Theories. | Philippe Suter, Robin Steiger, Viktor Kuncak |
| 2010 | CADE | MUNCH - Automated Reasoner for Sets and Multisets. | Ruzica Piskac, Viktor Kuncak |
| 2010 | CAV | Comfusy: A Tool for Complete Functional Synthesis. | Viktor Kuncak, Mikal Mayer, Ruzica Piskac, Philippe Suter |
| 2010 | CSL | Ordered Sets in the Calculus of Data Structures. | Viktor Kuncak, Ruzica Piskac, Philippe Suter |
| 2010 | FMCAD | Synthesis for regular specifications over unbounded domains. | Jad Hamza, Barbara Jobstmann, Viktor Kuncak |
| 2010 | ICSE | Test generation through programming in UDITA. | Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, Darko Marinov |
| 2010 | PLDI | Complete functional synthesis. | Viktor Kuncak, Mikal Mayer, Ruzica Piskac, Philippe Suter |
| 2010 | POPL | Decision procedures for algebraic data types with abstractions. | Philippe Suter, Mirco Dotta, Viktor Kuncak |
| 2010 | RV | Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. | Etienne Kneuss, Philippe Suter, Viktor Kuncak |
| 2010 | VMCAI | Building a Calculus of Data Structures. | Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies |
| 2010 | VMCAI | Collections, Cardinalities, and Relations. | Kuat Yessenov, Ruzica Piskac, Viktor Kuncak |
| 2009 | HotOS | Simplifying Distributed System Development. | Maysam Yabandeh, Nedeljko Vasic, Dejan Kostic, Viktor Kuncak |
| 2009 | NSDI | CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. | Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak |
| 2009 | PLDI | An integrated proof language for imperative programs. | Karen Zee, Viktor Kuncak, Martin C. Rinard |
| 2008 | CAV | Linear Arithmetic with Stars. | Ruzica Piskac, Viktor Kuncak |
| 2008 | CSL | Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars. | Ruzica Piskac, Viktor Kuncak |
| 2008 | PLDI | Full functional verification of linked data structures. | Karen Zee, Viktor Kuncak, Martin C. Rinard |
| 2008 | VMCAI | Runtime Checking for Separation Logic. | Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin |
| 2008 | VMCAI | Decision Procedures for Multisets with Cardinality Constraints. | Ruzica Piskac, Viktor Kuncak |
| 2007 | CADE | Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. | Viktor Kuncak, Martin C. Rinard |
| 2007 | FOSSACS | Polynomial Constraints for Sets with Cardinality Bounds. | Bruno Marnette, Viktor Kuncak, Martin C. Rinard |
| 2007 | RV | Runtime Checking for Program Verification. | Karen Zee, Viktor Kuncak, Michael B. Taylor, Martin C. Rinard |
| 2007 | VMCAI | Using First-Order Theorem Provers in the Jahob Data Structure Verification System. | Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard |
| 2006 | VMCAI | Field Constraint Analysis. | Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard |
| 2005 | CADE | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. | Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard |
| 2005 | CC | Hob: A Tool for Verifying Data Structure Consistency. | Patrick Lam, Viktor Kuncak, Martin C. Rinard |
| 2005 | VMCAI | Generalized Typestate Checking for Data Structure Consistency. | Patrick Lam, Viktor Kuncak, Martin C. Rinard |
| 2004 | ICFEM | Verifying a File System Implementation. | Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard |
| 2004 | SAS | Generalized Records and Spatial Conjunction in Role Logic. | Viktor Kuncak, Martin C. Rinard |
| 2004 | VMCAI | Boolean Algebra of Shape Analysis Constraints. | Viktor Kuncak, Martin C. Rinard |
| 2003 | LICS | Structural Subtyping of Non-Recursive Types is Decidable. | Viktor Kuncak, Martin C. Rinard |
| 2003 | SAS | Existential Heap Abstraction Entailment Is Undecidable. | Viktor Kuncak, Martin C. Rinard |
| 2002 | POPL | Role analysis. | Viktor Kuncak, Patrick Lam, Martin C. Rinard |