Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDViktor Kuncak
Viktor Kunčak
Person information
- affiliation: EPFL, Switzerland
- unicode name: Viktor Kunčak
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[j19]Dragana Milovancevic
, Viktor Kuncak:
Proving and Disproving Equivalence of Functional Programming Assignments. Proc. ACM Program. Lang. 7(PLDI): 928-951 (2023)- [c102]Simon Guilloud, Mario Bucev, Dragana Milovancevic, Viktor Kuncak:
Formula Normalizations in Verification. CAV (3) 2023: 398-422 - [c101]Simon Guilloud, Sankalp Gambhir, Viktor Kuncak:
LISA - A Modern Proof System. ITP 2023: 17:1-17:19 - [c100]Rodrigo Raya, Jad Hamza, Viktor Kuncak:
On the Complexity of Convex and Reverse Convex Prequadratic Constraints. LPAR 2023: 350-368 - [i35]Simon Guilloud, Viktor Kuncak:
Orthologic with Axioms. CoRR abs/2307.07569 (2023) - 2022
- [c99]Mario Bucev, Viktor Kuncak:
Formally Verified Quite OK Image Format. FMCAD 2022: 343-348 - [c98]Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer, Filip Schramka:
From Verified Scala to STIX File System Embedded Code Using Stainless. NFM 2022: 393-410 - [c97]Simon Guilloud, Viktor Kuncak:
Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. TACAS (2) 2022: 196-214 - [c96]Rodrigo Raya, Viktor Kuncak:
NP Satisfiability for Arrays as Powers. VMCAI 2022: 301-318 - [c95]Georg Stefan Schmid, Viktor Kuncak:
Generalized Arrays for Stainless Frames. VMCAI 2022: 332-354 - [i34]Rodrigo Raya, Jad Hamza, Viktor Kuncak:
NP Decision Procedure for Monomial and Linear Integer Constraints. CoRR abs/2208.02713 (2022) - 2021
- [c94]Viktor Kuncak, Jad Hamza:
Stainless Verification System Tutorial. FMCAD 2021: 2-7 - [i33]Georg Stefan Schmid, Viktor Kuncak:
Proving and Disproving Programs with Shared Mutable Data. CoRR abs/2103.07699 (2021) - [i32]Samuel Chassot, Viktor Kuncak:
Verified Mutable Data Structures. CoRR abs/2107.08824 (2021) - [i31]Rodrigo Raya, Viktor Kuncak:
NP Satisfiability for Arrays as Powers. CoRR abs/2109.05363 (2021) - [i30]Simon Guilloud, Viktor Kuncak:
On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. CoRR abs/2110.03315 (2021) - 2020
- [c93]Romain Edelmann, Jad Hamza, Viktor Kuncak:
Zippy LL(1) parsing with derivatives. PLDI 2020: 1036-1051 - [i29]Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza, Viktor Kuncak:
Coming to Terms with Your Choices: An Existential Take on Dependent Types. CoRR abs/2011.07653 (2020)
2010 – 2019
- 2019
- [j18]Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2): 73-102 (2019) - [j17]Jad Hamza, Nicolas Voirol, Viktor Kuncak:
System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA): 166:1-166:30 (2019) - [c92]Jad Hamza, Viktor Kuncak:
Minimal Synthesis of String to String Functions from Examples. VMCAI 2019: 48-69 - [i28]Romain Edelmann, Viktor Kuncak:
Neural-Network Guided Expression Transformation. CoRR abs/1902.02194 (2019) - [i27]Slobodan Mitrovic, Ruzica Piskac, Viktor Kuncak:
Identifying Maximal Non-Redundant Integer Cone Generators. CoRR abs/1903.08571 (2019) - [i26]Jad Hamza, Nicolas Voirol, Viktor Kuncak:
System FR as Foundations for Stainless. CoRR abs/1904.03482 (2019) - [i25]Romain Edelmann, Jad Hamza, Viktor Kuncak:
LL(1) Parsing with Derivatives and Zippers. CoRR abs/1911.12737 (2019) - 2018
- [j16]Mikaël Mayer, Viktor Kuncak, Ravi Chugh:
Bidirectional evaluation with direct manipulation. Proc. ACM Program. Lang. 2(OOPSLA): 127:1-127:28 (2018) - [i24]Mikaël Mayer, Viktor Kuncak, Ravi Chugh:
Bidirectional Evaluation with Direct Manipulation. CoRR abs/1809.04209 (2018) - 2017
- [j15]Mikaël Mayer, Jad Hamza, Viktor Kuncak:
Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact). Dagstuhl Artifacts Ser. 3(2): 16:1-16:2 (2017) - [j14]Andrew Reynolds, Tim King, Viktor Kuncak:
Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3): 500-532 (2017) - [j13]Eva Darulova, Viktor Kuncak:
Towards a Compiler for Reals. ACM Trans. Program. Lang. Syst. 39(2): 8:1-8:28 (2017) - [c91]Mikaël Mayer, Jad Hamza, Viktor Kuncak:
Proactive Synthesis of Recursive Tree-to-String Functions from Examples. ECOOP 2017: 19:1-19:30 - [c90]Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak:
Contract-based resource verification for higher-order functions with memoization. POPL 2017: 330-343 - [e4]Rupak Majumdar, Viktor Kuncak:
Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science 10426, Springer 2017, ISBN 978-3-319-63386-2 [contents] - [e3]Rupak Majumdar, Viktor Kuncak:
Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science 10427, Springer 2017, ISBN 978-3-319-63389-3 [contents] - [i23]Mikaël Mayer, Jad Hamza, Viktor Kuncak:
Polynomial-Time Proactive Synthesis of Tree-to-String Functions from Examples. CoRR abs/1701.04288 (2017) - [i22]Manos Koukoutos, Mukund Raghothaman, Etienne Kneuss, Viktor Kuncak:
On Repair with Probabilistic Attribute Grammars. CoRR abs/1707.04148 (2017) - [i21]Jad Hamza, Viktor Kuncak:
Minimal Synthesis of String To String Functions From Examples. CoRR abs/1710.09208 (2017) - 2016
- [c89]Lars Hupel, Viktor Kuncak:
Translating Scala Programs to Isabelle/HOL - System Description. IJCAR 2016: 568-577 - [c88]Georg Stefan Schmid, Viktor Kuncak:
SMT-based checking of predicate-qualified types for Scala. SCALA@SPLASH 2016: 31-40 - [c87]Manos Koukoutos, Etienne Kneuss, Viktor Kuncak:
An Update on Deductive Synthesis and Repair in the Leon Tool. SYNT@CAV 2016: 100-111 - [e2]Pavol Cerný, Viktor Kuncak, Parthasarathy Madhusudan:
Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015. EPTCS 202, 2016 [contents] - [i20]Lars Hupel, Viktor Kuncak:
Translating Scala Programs to Isabelle/HOL. CoRR abs/1607.01539 (2016) - 2015
- [j12]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
On recursion-free Horn clauses and Craig interpolation. Formal Methods Syst. Des. 47(1): 1-25 (2015) - [c86]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c85]Etienne Kneuss, Manos Koukoutos, Viktor Kuncak:
Deductive Program Repair. CAV (2) 2015: 217-233 - [c84]Tihomir Gvero, Viktor Kuncak:
Interactive Synthesis Using Free-Form Queries. ICSE (2) 2015: 689-692 - [c83]Viktor Kuncak:
Developing Verified Software Using Leon. NFM 2015: 12-15 - [c82]Ivan Kuraj, Viktor Kuncak, Daniel Jackson:
Programming with enumerable sets of structures. OOPSLA 2015: 37-56 - [c81]Ravichandhran Madhavan, Mikaël Mayer, Sumit Gulwani, Viktor Kuncak:
Automating grammar comparison. OOPSLA 2015: 183-200 - [c80]Tihomir Gvero, Viktor Kuncak:
Synthesizing Java expressions from free-form queries. OOPSLA 2015: 416-432 - [c79]Nicolas Voirol, Etienne Kneuss, Viktor Kuncak:
Counter-example complete verification for higher-order functions. Scala@PLDI 2015: 18-29 - [c78]Régis Blanc, Viktor Kuncak:
Sound reasoning about integral data types with a reusable SMT solver interface. Scala@PLDI 2015: 35-40 - [c77]Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac:
InSynth: A System for Code Completion using Types and Weights. Software Engineering & Management 2015: 39-40 - [c76]Andrew Reynolds, Viktor Kuncak:
Induction for SMT Solvers. VMCAI 2015: 80-98 - [i19]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli:
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR abs/1502.04464 (2015) - [i18]Andrew Reynolds, Tim King, Viktor Kuncak:
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. CoRR abs/1510.02642 (2015) - 2014
- [c75]Ravichandhran Madhavan, Viktor Kuncak:
Symbolic Resource Bound Inference for Functional Programs. CAV 2014: 762-778 - [c74]Ivan Kuraj, Viktor Kuncak:
SciFe: Scala framework for efficient enumeration of data structures with invariants. SCALA@ECOOP 2014: 45-49 - [c73]Viktor Kuncak:
Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution). ICALP (1) 2014: 11-25 - [c72]Eva Darulova, Viktor Kuncak:
Sound compilation of reals. POPL 2014: 235-248 - [c71]Emmanouil Koukoutos, Viktor Kuncak:
Checking Data Structure Properties Orders of Magnitude Faster. RV 2014: 263-268 - [i17]Eva Darulova, Viktor Kuncak:
On Numerical Error Propagation with Sensitivity. CoRR abs/1410.0198 (2014) - 2013
- [j11]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): 1004-1016 (2013) - [j10]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): 455-474 (2013) - [c70]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Disjunctive Interpolants for Horn-Clause Verification. CAV 2013: 347-363 - [c69]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: 1:1-1:10 - [c68]Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha:
Synthesis of fixed-point programs. EMSOFT 2013: 22:1-22:10 - [c67]Viktor Kuncak, Régis Blanc:
Interpolation for synthesis on unbounded domains. FMCAD 2013: 93-96 - [c66]Mikaël Mayer, Viktor Kuncak:
Game programming by demonstration. Onward! 2013: 75-90 - [c65]Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, Philippe Suter:
Synthesis modulo recursive functions. OOPSLA 2013: 407-426 - [c64]Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac:
Complete completion using types and weights. PLDI 2013: 27-38 - [c63]Viktor Kuncak, Etienne Kneuss, Philippe Suter:
Executing Specifications Using Synthesis and Constraint Solving. RV 2013: 1-20 - [c62]Yannis Klonatos, Andres Nötzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak:
Automatic synthesis of out-of-core algorithms. SIGMOD Conference 2013: 133-144 - [c61]Swen Jacobs, Viktor Kuncak, Philippe Suter:
Reductions for Synthesis Procedures. VMCAI 2013: 88-107 - [c60]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Classifying and Solving Horn Clauses for Verification. VSTTE 2013: 1-21 - [c59]Etienne Kneuss, Viktor Kuncak, Philippe Suter:
Effect Analysis for Programs with Callbacks. VSTTE 2013: 48-67 - [i16]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report). CoRR abs/1301.4973 (2013) - [i15]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses. CoRR abs/1302.4187 (2013) - [i14]Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, Philippe Suter:
On Integrating Deductive Synthesis and Verification Systems. CoRR abs/1304.5661 (2013) - [i13]Eva Darulova, Viktor Kuncak:
On Sound Compilation of Reals. CoRR abs/1309.2511 (2013) - 2012
- [j9]Rachid Guerraoui, Viktor Kuncak, Giuliano Losa:
Abortable Linearizable Modules. Arch. Formal Proofs 2012 (2012) - [j8]Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter:
Software synthesis procedures. Commun. ACM 55(2): 103-111 (2012) - [c58]Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer:
Accelerating Interpolants. ATVA 2012: 187-202 - [c57]Andrej Spielmann, Viktor Kuncak:
Synthesis for Unbounded Bit-Vector Arithmetic. IJCAR 2012: 499-513 - [c56]Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer:
A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM 2012: 247-251 - [c55]Rachid Guerraoui, Viktor Kuncak, Giuliano Losa:
Speculative linearizability. PLDI 2012: 55-66 - [c54]Ali Sinan Köksal, Viktor Kuncak, Philippe Suter:
Constraints as control. POPL 2012: 151-164 - [c53]Eva Darulova, Viktor Kuncak:
Certifying Solutions for Numerical Constraints. RV 2012: 277-291 - [c52]Thomas Wies, Marco Muñiz, Viktor Kuncak:
Deciding Functional Lists with Sublist Sets. VSTTE 2012: 66-81 - [c51]Milena Vujosevic-Janicic, Viktor Kuncak:
Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description. VSTTE 2012: 98-113 - [e1]Viktor Kuncak, Andrey Rybalchenko:
Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings. Lecture Notes in Computer Science 7148, Springer 2012, ISBN 978-3-642-27939-3 [contents] - [i12]Milena Vujosevic-Janicic, Mladen Nikolic, Dusan Tosic, Viktor Kuncak:
Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. CoRR abs/1206.7064 (2012) - 2011
- [c50]Ali Sinan Köksal, Viktor Kuncak, Philippe Suter:
Scala to the Power of Z3: Integrating SMT and Programming. CADE 2011: 400-406 - [c49]Thomas Wies, Marco Muñiz, Viktor Kuncak:
An Efficient Decision Procedure for Imperative Tree Data Structures. CADE 2011: 476-491 - [c48]Tihomir Gvero, Viktor Kuncak, Ruzica Piskac:
Interactive Synthesis of Code Snippets. CAV 2011: 418-423 - [c47]Eva Darulova, Viktor Kuncak:
Trustworthy numerical computation in Scala. OOPSLA 2011: 325-344 - [c46]Philippe Suter, Ali Sinan Köksal, Viktor Kuncak:
Satisfiability Modulo Recursive Programs. SAS 2011: 298-315 - [c45]Swen Jacobs, Viktor Kuncak:
Towards Complete Reasoning about Axiomatic Specifications. VMCAI 2011: 278-293 - [c44]Philippe Suter, Robin Steiger, Viktor Kuncak:
Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI 2011: 403-418 - 2010
- [j7]Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak:
Predicting and preventing inconsistencies in deployed distributed systems. ACM Trans. Comput. Syst. 28(1): 2:1-2:49 (2010) - [c43]Ruzica Piskac, Viktor Kuncak:
MUNCH - Automated Reasoner for Sets and Multisets. IJCAR 2010: 149-155 - [c42]Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter:
Comfusy: A Tool for Complete Functional Synthesis. CAV 2010: 430-433 - [c41]Viktor Kuncak, Ruzica Piskac, Philippe Suter:
Ordered Sets in the Calculus of Data Structures. CSL 2010: 34-48 - [c40]Jad Hamza, Barbara Jobstmann, Viktor Kuncak:
Synthesis for regular specifications over unbounded domains. FMCAD 2010: 101-109 - [c39]Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, Darko Marinov:
Test generation through programming in UDITA. ICSE (1) 2010: 225-234 - [c38]Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter:
Complete functional synthesis. PLDI 2010: 316-329 - [c37]Philippe Suter, Mirco Dotta, Viktor Kuncak:
Decision procedures for algebraic data types with abstractions. POPL 2010: 199-210 - [c36]Etienne Kneuss, Philippe Suter, Viktor Kuncak:
Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. RV 2010: 300-314 - [c35]Etienne Kneuss, Philippe Suter, Viktor Kuncak:
Phantm: PHP analyzer for type mismatch. SIGSOFT FSE 2010: 373-374 - [c34]Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies:
Building a Calculus of Data Structures. VMCAI 2010: 26-44 - [c33]Kuat Yessenov, Ruzica Piskac, Viktor Kuncak:
Collections, Cardinalities, and Relations. VMCAI 2010: 380-395
2000 – 2009
- 2009
- [c32]Thomas Wies, Ruzica Piskac, Viktor Kuncak:
Combining Theories with Shared Set Operations. FroCoS 2009: 366-382 - [c31]Maysam Yabandeh, Nedeljko Vasic, Dejan Kostic, Viktor Kuncak:
Simplifying Distributed System Development. HotOS 2009 - [c30]Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak:
CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. NSDI 2009: 229-244 - [c29]Karen Zee, Viktor Kuncak, Martin C. Rinard:
An integrated proof language for imperative programs. PLDI 2009: 338-351 - [c28]Pierre-Évariste Dagand, Dejan Kostic, Viktor Kuncak:
Opis: reliable distributed systems in OCaml. TLDI 2009: 65-78 - 2008
- [c27]Ruzica Piskac, Viktor Kuncak:
Linear Arithmetic with Stars. CAV 2008: 268-280 - [c26]Ruzica Piskac, Viktor Kuncak:
Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars. CSL 2008: 124-138 - [c25]Karen Zee, Viktor Kuncak, Martin C. Rinard:
Verifying linked data structure implementations. IPDPS 2008: 1-5 - [c24]Karen Zee, Viktor Kuncak, Martin C. Rinard:
Full functional verification of linked data structures. PLDI 2008: 349-361 - [c23]Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin:
Runtime Checking for Separation Logic.