Viktor Kuncak

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 60

Top Venues

CoRR

VMCAI

Proc. ACM Program. Lang.

OOPSLA

Massachusetts Institute of Technology, Cambridge, MA, USA (PHD)

Education History

Massachusetts Institute of Technology, Cambridge, MA, USA

PHD

Publications

Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
Interpolation and Quantifiers in Ortholattices. VMCAI (1) (2024)
Rodrigo Raya, Viktor Kuncak
Succinct ordering and aggregation constraints in algebraic array theories. J. Log. Algebraic Methods Program. 140 (2024)
Simon Guilloud, Viktor Kuncak
Orthologic with Axioms. Proc. ACM Program. Lang. 8 (POPL) (2024)
Auguste Poiroux, Gail Weiss, Viktor Kuncak, Antoine Bosselut
Improving Autoformalization using Type Checking. CoRR (2024)
Rodrigo Raya, Viktor Kuncak
On algebraic array theories. J. Log. Algebraic Methods Program. 136 (2024)
Samuel Chassot, Viktor Kuncak
Verifying a Realistic Mutable Hash Table - Case Study (Short Paper). IJCAR (1) (2024)
Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak
Mechanized HOL Reasoning in Set Theory. CoRR (2024)
Simon Guilloud, Mario Bucev, Dragana Milovancevic, Viktor Kuncak
Formula Normalizations in Verification. CAV (3) (2023)
Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
LISA - A Modern Proof System. ITP (2023)
Dragana Milovancevic, Viktor Kuncak
Proving and Disproving Equivalence of Functional Programming Assignments. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Simon Guilloud, Viktor Kuncak
Orthologic with Axioms. CoRR (2023)
Rodrigo Raya, Jad Hamza, Viktor Kuncak
On the Complexity of Convex and Reverse Convex Prequadratic Constraints. LPAR (2023)
Georg Stefan Schmid, Viktor Kuncak
Generalized Arrays for Stainless Frames. VMCAI (2022)
Rodrigo Raya, Viktor Kuncak
NP Satisfiability for Arrays as Powers. VMCAI (2022)
Rodrigo Raya, Jad Hamza, Viktor Kuncak
NP Decision Procedure for Monomial and Linear Integer Constraints. CoRR (2022)
Simon Guilloud, Viktor Kuncak
Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. TACAS (2) (2022)
Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer, Filip Schramka
From Verified Scala to STIX File System Embedded Code Using Stainless. NFM (2022)
Mario Bucev, Viktor Kuncak
Formally Verified Quite OK Image Format. FMCAD (2022)
Viktor Kuncak, Jad Hamza
Stainless Verification System Tutorial. FMCAD (2021)
Rodrigo Raya, Viktor Kuncak
NP Satisfiability for Arrays as Powers. CoRR (2021)
Simon Guilloud, Viktor Kuncak
On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. CoRR (2021)
Samuel Chassot, Viktor Kuncak
Verified Mutable Data Structures. CoRR (2021)
Georg Stefan Schmid, Viktor Kuncak
Proving and Disproving Programs with Shared Mutable Data. CoRR (2021)
Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza, Viktor Kuncak
Coming to Terms with Your Choices: An Existential Take on Dependent Types. CoRR (2020)
Romain Edelmann, Jad Hamza, Viktor Kuncak
Zippy LL(1) parsing with derivatives. PLDI (2020)
Jad Hamza, Nicolas Voirol, Viktor Kuncak
System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Jad Hamza, Nicolas Voirol, Viktor Kuncak
System FR as Foundations for Stainless. CoRR (2019)
Romain Edelmann, Viktor Kuncak
Neural-Network Guided Expression Transformation. CoRR (2019)
Slobodan Mitrovic, Ruzica Piskac, Viktor Kuncak
Identifying Maximal Non-Redundant Integer Cone Generators. CoRR (2019)
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55 (2) (2019)
Jad Hamza, Viktor Kuncak
Minimal Synthesis of String to String Functions from Examples. VMCAI (2019)
Romain Edelmann, Jad Hamza, Viktor Kuncak
LL(1) Parsing with Derivatives and Zippers. CoRR (2019)
Mikaël Mayer, Viktor Kuncak, Ravi Chugh
Bidirectional Evaluation with Direct Manipulation. CoRR (2018)
Mikaël Mayer, Viktor Kuncak, Ravi Chugh
Bidirectional evaluation with direct manipulation. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Jad Hamza, Viktor Kuncak
Minimal Synthesis of String To String Functions From Examples. CoRR (2017)
Manos Koukoutos, Mukund Raghothaman, Etienne Kneuss, Viktor Kuncak
On Repair with Probabilistic Attribute Grammars. CoRR (2017)
Andrew Reynolds, Tim King, Viktor Kuncak
Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51 (3) (2017)
Eva Darulova, Viktor Kuncak
Towards a Compiler for Reals. ACM Trans. Program. Lang. Syst. 39 (2) (2017)
Mikaël Mayer, Jad Hamza, Viktor Kuncak
Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact). Dagstuhl Artifacts Ser. 3 (2) (2017)
Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak
Contract-based resource verification for higher-order functions with memoization. POPL (2017)
Mikaël Mayer, Jad Hamza, Viktor Kuncak
Proactive Synthesis of Recursive Tree-to-String Functions from Examples. ECOOP (2017)
Mikaël Mayer, Jad Hamza, Viktor Kuncak
Polynomial-Time Proactive Synthesis of Tree-to-String Functions from Examples. CoRR (2017)
Lars Hupel, Viktor Kuncak
Translating Scala Programs to Isabelle/HOL. CoRR (2016)
Georg Stefan Schmid, Viktor Kuncak
SMT-based checking of predicate-qualified types for Scala. SCALA@SPLASH (2016)
Lars Hupel, Viktor Kuncak
Translating Scala Programs to Isabelle/HOL - System Description. IJCAR (2016)
Manos Koukoutos, Etienne Kneuss, Viktor Kuncak
An Update on Deductive Synthesis and Repair in the Leon Tool. SYNT@CAV (2016)
Nicolas Voirol, Etienne Kneuss, Viktor Kuncak
Counter-example complete verification for higher-order functions. Scala@PLDI (2015)
Andrew Reynolds, Tim King, Viktor Kuncak
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. CoRR (2015)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR (2015)
Ivan Kuraj, Viktor Kuncak, Daniel Jackson
Programming with enumerable sets of structures. OOPSLA (2015)
Tihomir Gvero, Viktor Kuncak
Synthesizing Java expressions from free-form queries. OOPSLA (2015)
Tihomir Gvero, Viktor Kuncak
Interactive Synthesis Using Free-Form Queries. ICSE (2) (2015)
Etienne Kneuss, Manos Koukoutos, Viktor Kuncak
Deductive Program Repair. CAV (2) (2015)
Andrew Reynolds, Viktor Kuncak
Induction for SMT Solvers. VMCAI (2015)
Ravichandhran Madhavan, Mikaël Mayer, Sumit Gulwani, Viktor Kuncak
Automating grammar comparison. OOPSLA (2015)
Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac
InSynth: A System for Code Completion using Types and Weights. Software Engineering & Management (2015)
Viktor Kuncak
Developing Verified Software Using Leon. NFM (2015)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) (2015)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
On recursion-free Horn clauses and Craig interpolation. Formal Methods Syst. Des. 47 (1) (2015)
Régis Blanc, Viktor Kuncak
Sound reasoning about integral data types with a reusable SMT solver interface. Scala@PLDI (2015)
Eva Darulova, Viktor Kuncak
Sound compilation of reals. POPL (2014)
Ivan Kuraj, Viktor Kuncak
SciFe: Scala framework for efficient enumeration of data structures with invariants. SCALA@ECOOP (2014)
Viktor Kuncak
Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution). ICALP (1) (2014)
Ravichandhran Madhavan, Viktor Kuncak
Symbolic Resource Bound Inference for Functional Programs. CAV (2014)
Eva Darulova, Viktor Kuncak
On Numerical Error Propagation with Sensitivity. CoRR (2014)
Emmanouil Koukoutos, Viktor Kuncak
Checking Data Structure Properties Orders of Magnitude Faster. RV (2014)
Viktor Kuncak, Etienne Kneuss, Philippe Suter
Executing Specifications Using Synthesis and Constraint Solving. RV (2013)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
Disjunctive Interpolants for Horn-Clause Verification. CAV (2013)
Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha
Synthesis of fixed-point programs. EMSOFT (2013)
Etienne Kneuss, Viktor Kuncak, Philippe Suter
Effect Analysis for Programs with Callbacks. VSTTE (2013)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report) CoRR (2013)
Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac
Complete completion using types and weights. PLDI (2013)
Yannis Klonatos, Andres Nötzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak
Automatic synthesis of out-of-core algorithms. SIGMOD Conference (2013)
Eva Darulova, Viktor Kuncak
On Sound Compilation of Reals. CoRR (2013)
Swen Jacobs, Viktor Kuncak, Philippe Suter
Reductions for Synthesis Procedures. VMCAI (2013)
Régis Blanc, Viktor Kuncak, Etienne Kneuss, Philippe Suter
An overview of the Leon verification system: verification by translation to recursive functions. SCALA@ECOOP (2013)
Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, Philippe Suter
On Integrating Deductive Synthesis and Verification Systems CoRR (2013)
Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, Philippe Suter
Synthesis modulo recursive functions. OOPSLA (2013)
Mikaël Mayer, Viktor Kuncak
Game programming by demonstration. Onward! (2013)
Milena Vujosevic-Janicic, Mladen Nikolic, Dusan Tosic, Viktor Kuncak
Software verification and graph similarity for automated evaluation of students' assignments. Inf. Softw. Technol. 55 (6) (2013)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
Classifying and Solving Horn Clauses for Verification. VSTTE (2013)
Viktor Kuncak, Régis Blanc
Interpolation for synthesis on unbounded domains. FMCAD (2013)
Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
Functional synthesis for linear arithmetic and sets. Int. J. Softw. Tools Technol. Transf. 15 (5-6) (2013)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses CoRR (2013)
Ali Sinan Köksal, Viktor Kuncak, Philippe Suter
Constraints as control. POPL (2012)
Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer
Accelerating Interpolants. ATVA (2012)
Rachid Guerraoui, Viktor Kuncak, Giuliano Losa
Abortable Linearizable Modules. Arch. Formal Proofs 2012 (2012)
Milena Vujosevic-Janicic, Viktor Kuncak
Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description. VSTTE (2012)
Rachid Guerraoui, Viktor Kuncak, Giuliano Losa
Speculative linearizability. PLDI (2012)
Milena Vujosevic-Janicic, Mladen Nikolic, Dusan Tosic, Viktor Kuncak
Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. CoRR (2012)
Eva Darulova, Viktor Kuncak
Certifying Solutions for Numerical Constraints. RV (2012)
Andrej Spielmann, Viktor Kuncak
Synthesis for Unbounded Bit-Vector Arithmetic. IJCAR (2012)
Thomas Wies, Marco Muñiz, Viktor Kuncak
Deciding Functional Lists with Sublist Sets. VSTTE (2012)
Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
Software synthesis procedures. Commun. ACM 55 (2) (2012)
Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer
A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM (2012)
Tihomir Gvero, Viktor Kuncak, Ruzica Piskac
Interactive Synthesis of Code Snippets. CAV (2011)
Thomas Wies, Marco Muñiz, Viktor Kuncak
An Efficient Decision Procedure for Imperative Tree Data Structures. CADE (2011)
Philippe Suter, Robin Steiger, Viktor Kuncak
Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI (2011)
Swen Jacobs, Viktor Kuncak
Towards Complete Reasoning about Axiomatic Specifications. VMCAI (2011)
Ali Sinan Köksal, Viktor Kuncak, Philippe Suter
Scala to the Power of Z3: Integrating SMT and Programming. CADE (2011)

Viktor Kuncak.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Viktor Kuncak