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
- 2024
[j22]Rodrigo Raya
, Viktor Kuncak:
On algebraic array theories. J. Log. Algebraic Methods Program. 136: 100906 (2024)- [j21]Rodrigo Raya, Viktor Kuncak:
Succinct ordering and aggregation constraints in algebraic array theories. J. Log. Algebraic Methods Program. 140: 100978 (2024) - [j20]Simon Guilloud, Viktor Kuncak:
Orthologic with Axioms. Proc. ACM Program. Lang. 8(POPL): 1150-1178 (2024) - [c106]Dragana Milovancevic, Carsten Fuhs, Mario Bucev, Viktor Kuncak:
Proving Termination via Measure Transfer in Equivalence Checking. IFM 2024: 75-84 - [c105]Samuel Chassot, Viktor Kuncak:
Verifying a Realistic Mutable Hash Table - Case Study (Short Paper). IJCAR (1) 2024: 304-314 - [c104]Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak:
Mechanized HOL Reasoning in Set Theory. ITP 2024: 18:1-18:18 - [c103]Simon Guilloud, Sankalp Gambhir, Viktor Kuncak:
Interpolation and Quantifiers in Ortholattices. VMCAI (1) 2024: 235-257 - [i38]Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak:
Mechanized HOL Reasoning in Set Theory. CoRR abs/2403.13403 (2024) - [i37]Auguste Poiroux, Gail Weiss, Viktor Kuncak, Antoine Bosselut:
Improving Autoformalization using Type Checking. CoRR abs/2406.07222 (2024) - [i36]Beatriz Borges, Negar Foroutan, Deniz Bayazit, Anna Sotnikova, Syrielle Montariol, Tanya Nazaretzky, Mohammadreza Banaei, Alireza Sakhaeirad, Philippe Servant, Seyed Parsa Neshaei, Jibril Frej, Angelika Romanou, Gail Weiss, Sepideh Mamooler, Zeming Chen, Simin Fan, Silin Gao, Mete Ismayilzada, Debjit Paul, Alexandre Schöpfer, Andrej Janchevski, Anja Tiede, Clarence Linden, Emanuele Troiani, Francesco Salvi, Freya Behrens, Giacomo Orsi, Giovanni Piccioli, Hadrien Sevel, Louis Coulon, Manuela Pineros-Rodriguez, Marin Bonnassies, Pierre Hellich, Puck van Gerwen, Sankalp Gambhir, Solal Pirelli, Thomas Blanchard, Timothée Callens, Toni Abi Aoun, Yannick Calvino Alonso, Yuri Cho, Alberto Silvio Chiappa, Antonio Sclocchi, Étienne Bruno, Florian Hofhammer, Gabriel Pescia, Geovani Rizk, Leello Dadi, Lucas Stoffl, Manoel Horta Ribeiro, Matthieu Bovel, Yueyang Pan, Aleksandra Radenovic, Alexandre Alahi, Alexander Mathis, Anne-Florence Bitbol, Boi Faltings, Cécile Hébert, Devis Tuia, François Maréchal, George Candea, Giuseppe Carleo, Jean-Cédric Chappelier, Nicolas Flammarion, Jean-Marie Fürbringer, Jean-Philippe Pellet, Karl Aberer, Lenka Zdeborová, Marcel Salathé, Martin Jaggi, Martin Rajman, Mathias Payer, Matthieu Wyart, Michael Gastpar, Michele Ceriotti, Ola Svensson, Olivier Lévêque, Paolo Ienne, Rachid Guerraoui, Robert West, Sanidhya Kashyap, Valerio Piazza, Viesturs Simanis, Viktor Kuncak, Volkan Cevher, Philippe Schwaller, Sacha Friedli, Patrick Jermann, Tanja Käser, Antoine Bosselut:
Could ChatGPT get an Engineering Degree? Evaluating Higher Education Vulnerability to AI Assistants. CoRR abs/2408.11841 (2024) - 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. VMCAI 2008: 203-217 - [c22]Ruzica Piskac, Viktor Kuncak:
Decision Procedures for Multisets with Cardinality Constraints. VMCAI 2008: 218-232 - 2007
- [b1]Viktor Kuncak:
Modular data structure verification. Massachusetts Institute of Technology, Cambridge, MA, USA, 2007 - [c21]Viktor Kuncak, Martin C. Rinard:
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. CADE 2007: 215-230 - [c20]Bruno Marnette, Viktor Kuncak, Martin C. Rinard:
Polynomial Constraints for Sets with Cardinality Bounds. FoSSaCS 2007: 258-273 - [c19]Karen Zee, Viktor Kuncak, Michael B. Taylor, Martin C. Rinard:
Runtime Checking for Program Verification. RV 2007: 202-213 - [c18]Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard:
Using First-Order Theorem Provers in the Jahob Data Structure Verification System. VMCAI 2007: 74-88 - 2006
- [j6]Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard:
Deciding Boolean Algebra with Presburger Arithmetic. J. Autom. Reason. 36(3): 213-239 (2006) - [j5]Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard:
Modular Pluggable Analyses for Data Structure Consistency. IEEE Trans. Software Eng. 32(12): 988-1005 (2006) - [c17]Viktor Kuncak, Martin C. Rinard:
An overview of the Jahob analysis system: project goals and current status. IPDPS 2006 - [c16]Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard:
Field Constraint Analysis. VMCAI 2006: 157-173 - [i11]Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, Martin C. Rinard:
On Verifying Complex Properties using Symbolic Shape Analysis. CoRR abs/cs/0609104 (2006) - 2005
- [c15]Patrick Lam, Viktor Kuncak, Martin C. Rinard:
Crosscutting techniques in program specification and analysis. AOSD 2005: 169-180 - [c14]Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard:
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. CADE 2005: 260-277 - [c13]Patrick Lam, Viktor Kuncak, Martin C. Rinard:
Hob: A Tool for Verifying Data Structure Consistency. CC 2005: 237-241 - [c12]Viktor Kuncak, Daniel Jackson:
Relational analysis of algebraic datatypes. ESEC/SIGSOFT FSE 2005: 207-216 - [c11]Patrick Lam, Viktor Kuncak, Martin C. Rinard:
Generalized Typestate Checking for Data Structure Consistency. VMCAI 2005: 430-447 - [c10]Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard:
Implications of a Data Structure Consistency Checking System. VSTTE 2005: 214-226 - [c9]Viktor Kuncak, Martin C. Rinard:
Decision Procedures for Set-Valued Fields. AIOOL@VMCAI 2005: 51-62 - [i10]Viktor Kuncak, Martin C. Rinard, Bruno Marnette:
On Algorithms and Complexity for Sets with Cardinality Constraints. Deduction and Applications 2005 - [i9]Bruno Marnette, Viktor Kuncak, Martin C. Rinard:
On Algorithms and Complexity for Sets with Cardinality Constraints. CoRR abs/cs/0508123 (2005) - 2004
- [j4]Viktor Kuncak:
Binary Search Trees. Arch. Formal Proofs 2004 (2004) - [j3]Karen Zee, Viktor Kuncak:
File Refinement. Arch. Formal Proofs 2004 (2004) - [j2]Patrick Lam, Viktor Kuncak, Martin C. Rinard:
Generalized typestate checking using set interfaces and pluggable analyses. ACM SIGPLAN Notices 39(3): 46-55 (2004) - [c8]Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard:
Verifying a File System Implementation. ICFEM 2004: 373-390 - [c7]Viktor Kuncak, Martin C. Rinard:
Generalized Records and Spatial Conjunction in Role Logic. SAS 2004: 361-376 - [c6]Viktor Kuncak, Martin C. Rinard:
Boolean Algebra of Shape Analysis Constraints. VMCAI 2004: 59-72 - [i8]Viktor Kuncak, Martin C. Rinard:
The First-Order Theory of Sets with Cardinality Constraints is Decidable. CoRR cs.LO/0407045 (2004) - [i7]Viktor Kuncak, Martin C. Rinard:
On the Theory of Structural Subtyping. CoRR cs.LO/0408015 (2004) - [i6]Viktor Kuncak, Martin C. Rinard:
On Spatial Conjunction as Second-Order Logic. CoRR cs.LO/0410073 (2004) - [i5]Viktor Kuncak, Patrick Lam, Martin C. Rinard:
Roles Are Really Great! CoRR cs.PL/0408013 (2004) - [i4]Viktor Kuncak, Martin C. Rinard:
Typestate Checking and Regular Graph Constraints. CoRR cs.PL/0408014 (2004) - [i3]Viktor Kuncak, Martin C. Rinard:
On Role Logic. CoRR cs.PL/0408018 (2004) - [i2]Viktor Kuncak, Martin C. Rinard:
On Generalized Records and Spatial Conjunction in Role Logic. CoRR cs.PL/0408019 (2004) - [i1]Viktor Kuncak, K. Rustan M. Leino:
On computing the fixpoint of a set of boolean equations. CoRR cs.PL/0408045 (2004) - 2003
- [c5]Viktor Kuncak, Martin C. Rinard:
Structural Subtyping of Non-Recursive Types is Decidable. LICS 2003: 96-107 - [c4]Viktor Kuncak, Martin C. Rinard:
Existential Heap Abstraction Entailment Is Undecidable. SAS 2003: 418-438 - 2002
- [j1]Mirjana Ivanovic, Viktor Kuncak:
Numerical Representations as Purely Functional Data Structures: a New Approach. Informatica 13(2): 163-176 (2002) - [c3]Viktor Kuncak, Patrick Lam, Martin C. Rinard:
Role analysis. POPL 2002: 17-32 - 2001
- [c2]Silvia Ghilezan, Viktor Kuncak:
Confluence of Untyped Lambda Calculus via Simple Types. ICTCS 2001: 38-49 - [c1]Viktor Kuncak, Patrick Lam, Martin C. Rinard:
A Language for Role Specifications. LCPC 2001: 366-382
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-23 20:29 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
