Viktor Kuncak - RankMe

184 papers A* 18A 17B 38C 1Misc 2Journal 67Unranked 37

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Are Dependent Types in Set Theory Feasible? CoRR Yunsong Yang, Simon Guilloud, Viktor Kuncak
2025	—	`conf`	Formal Autograding in a Classroom. ESOP (2) Dragana Milovancevic, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, Viktor Kuncak
2025	—	`conf`	Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study. VMCAI (2) Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kuncak
2025	A	`conf`	Interoperability of Proof Systems with SC-TPTP. CADE Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak
2025	J	`jnl`	Interpolation and Quantifiers in Ortholattices. CoRR Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
2025	J	`jnl`	LISA - A Modern Proof System. CoRR Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
2025	J	`jnl`	Orthologic Type Systems. CoRR Simon Guilloud, Viktor Kuncak
2025	—	`conf`	RLMEval: Evaluating Research-Level Neural Theorem Proving. EMNLP (Findings) Auguste Poiroux, Antoine Bosselut, Viktor Kuncak
2025	J	`jnl`	RLMEval: Evaluating Research-Level Neural Theorem Proving. CoRR Auguste Poiroux, Antoine Bosselut, Viktor Kuncak
2025	A*	`conf`	Reliable Evaluation and Benchmarks for Statement Autoformalization. EMNLP Auguste Poiroux, Gail Weiss, Viktor Kuncak, Antoine Bosselut
2025	J	`jnl`	ZipLex: Verified Invertible Lexing with Memoized Derivatives and Zippers. CoRR Samuel Chassot, Viktor Kuncak
2024	J	`jnl`	Could ChatGPT get an Engineering Degree? Evaluating Higher Education Vulnerability to AI Assistants. CoRR 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
2024	J	`jnl`	Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study. CoRR Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kuncak
2024	J	`jnl`	Improving Autoformalization using Type Checking. CoRR Auguste Poiroux, Gail Weiss, Viktor Kuncak, Antoine Bosselut
2024	—	`conf`	Interpolation and Quantifiers in Ortholattices. VMCAI (1) Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
2024	B	`conf`	Mechanized HOL Reasoning in Set Theory. ITP Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak
2024	J	`jnl`	Mechanized HOL Reasoning in Set Theory. CoRR Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak
2024	J	`jnl`	On algebraic array theories. J. Log. Algebraic Methods Program. Rodrigo Raya, Viktor Kuncak
2024	J	`jnl`	Orthologic with Axioms. Proc. ACM Program. Lang. Simon Guilloud, Viktor Kuncak
2024	B	`conf`	Proving Termination via Measure Transfer in Equivalence Checking. IFM Dragana Milovancevic, Carsten Fuhs, Mario Bucev, Viktor Kuncak
2024	J	`jnl`	Succinct ordering and aggregation constraints in algebraic array theories. J. Log. Algebraic Methods Program. Rodrigo Raya, Viktor Kuncak
2024	J	`jnl`	Verified invertible lexer using regular expressions and DFAs. CoRR Samuel Chassot, Viktor Kuncak
2024	—	`conf`	Verifying a Realistic Mutable Hash Table - Case Study (Short Paper). IJCAR (1) Samuel Chassot, Viktor Kuncak
2023	—	`conf`	Formula Normalizations in Verification. CAV (3) Simon Guilloud, Mario Bucev, Dragana Milovancevic, Viktor Kuncak
2023	B	`conf`	LISA - A Modern Proof System. ITP Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
2023	B	`conf`	On the Complexity of Convex and Reverse Convex Prequadratic Constraints. LPAR Rodrigo Raya, Jad Hamza, Viktor Kuncak
2023	J	`jnl`	Orthologic with Axioms. CoRR Simon Guilloud, Viktor Kuncak
2023	J	`jnl`	Proving and Disproving Equivalence of Functional Programming Assignments. Proc. ACM Program. Lang. Dragana Milovancevic, Viktor Kuncak
2022	—	`conf`	Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. TACAS (2) Simon Guilloud, Viktor Kuncak
2022	B	`conf`	Formally Verified Quite OK Image Format. FMCAD Mario Bucev, Viktor Kuncak
2022	—	`conf`	From Verified Scala to STIX File System Embedded Code Using Stainless. NFM Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer, Filip Schramka
2022	B	`conf`	Generalized Arrays for Stainless Frames. VMCAI Georg Stefan Schmid, Viktor Kuncak
2022	J	`jnl`	NP Decision Procedure for Monomial and Linear Integer Constraints. CoRR Rodrigo Raya, Jad Hamza, Viktor Kuncak
2022	B	`conf`	NP Satisfiability for Arrays as Powers. VMCAI Rodrigo Raya, Viktor Kuncak
2021	J	`jnl`	NP Satisfiability for Arrays as Powers. CoRR Rodrigo Raya, Viktor Kuncak
2021	J	`jnl`	On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. CoRR Simon Guilloud, Viktor Kuncak
2021	J	`jnl`	Proving and Disproving Programs with Shared Mutable Data. CoRR Georg Stefan Schmid, Viktor Kuncak
2021	B	`conf`	Stainless Verification System Tutorial. FMCAD Viktor Kuncak, Jad Hamza
2021	J	`jnl`	Verified Mutable Data Structures. CoRR Samuel Chassot, Viktor Kuncak
2020	J	`jnl`	Coming to Terms with Your Choices: An Existential Take on Dependent Types. CoRR Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza, Viktor Kuncak
2020	A*	`conf`	Zippy LL(1) parsing with derivatives. PLDI Romain Edelmann, Jad Hamza, Viktor Kuncak
2019	J	`jnl`	Identifying Maximal Non-Redundant Integer Cone Generators. CoRR Slobodan Mitrovic, Ruzica Piskac, Viktor Kuncak
2019	J	`jnl`	LL(1) Parsing with Derivatives and Zippers. CoRR Romain Edelmann, Jad Hamza, Viktor Kuncak
2019	B	`conf`	Minimal Synthesis of String to String Functions from Examples. VMCAI Jad Hamza, Viktor Kuncak
2019	J	`jnl`	Neural-Network Guided Expression Transformation. CoRR Romain Edelmann, Viktor Kuncak
2019	J	`jnl`	Refutation-based synthesis in SMT. Formal Methods Syst. Des. Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2019	J	`jnl`	System FR as Foundations for Stainless. CoRR Jad Hamza, Nicolas Voirol, Viktor Kuncak
2019	J	`jnl`	System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. Jad Hamza, Nicolas Voirol, Viktor Kuncak
2018	J	`jnl`	Bidirectional Evaluation with Direct Manipulation. CoRR Mikaël Mayer, Viktor Kuncak, Ravi Chugh
2018	J	`jnl`	Bidirectional evaluation with direct manipulation. Proc. ACM Program. Lang. Mikaël Mayer, Viktor Kuncak, Ravi Chugh
2017	—	`ed.`	Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I CAV (1) Rupak Majumdar, Viktor Kuncak
2017	—	`ed.`	Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II CAV (2) Rupak Majumdar, Viktor Kuncak
2017	A*	`conf`	Contract-based resource verification for higher-order functions with memoization. POPL Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak
2017	J	`jnl`	Minimal Synthesis of String To String Functions From Examples. CoRR Jad Hamza, Viktor Kuncak
2017	J	`jnl`	On Repair with Probabilistic Attribute Grammars. CoRR Manos Koukoutos, Mukund Raghothaman, Etienne Kneuss, Viktor Kuncak
2017	J	`jnl`	Polynomial-Time Proactive Synthesis of Tree-to-String Functions from Examples. CoRR Mikaël Mayer, Jad Hamza, Viktor Kuncak
2017	J	`jnl`	Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact). Dagstuhl Artifacts Ser. Mikaël Mayer, Jad Hamza, Viktor Kuncak
2017	A	`conf`	Proactive Synthesis of Recursive Tree-to-String Functions from Examples. ECOOP Mikaël Mayer, Jad Hamza, Viktor Kuncak
2017	J	`jnl`	Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. Andrew Reynolds, Tim King, Viktor Kuncak
2017	J	`jnl`	Towards a Compiler for Reals. ACM Trans. Program. Lang. Syst. Eva Darulova, Viktor Kuncak
2016	—	`conf`	An Update on Deductive Synthesis and Repair in the Leon Tool. SYNT@CAV Manos Koukoutos, Etienne Kneuss, Viktor Kuncak
2016	—	`ed.`	Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015. SYNT Pavol Cerný, Viktor Kuncak, Parthasarathy Madhusudan
2016	—	`conf`	SMT-based checking of predicate-qualified types for Scala. SCALA@SPLASH Georg Stefan Schmid, Viktor Kuncak
2016	A	`conf`	Translating Scala Programs to Isabelle/HOL - System Description. IJCAR Lars Hupel, Viktor Kuncak
2016	J	`jnl`	Translating Scala Programs to Isabelle/HOL. CoRR Lars Hupel, Viktor Kuncak
2015	J	`jnl`	An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. CoRR Andrew Reynolds, Tim King, Viktor Kuncak
2015	A	`conf`	Automating grammar comparison. OOPSLA Ravichandhran Madhavan, Mikaël Mayer, Sumit Gulwani, Viktor Kuncak
2015	—	`conf`	Counter-example complete verification for higher-order functions. Scala@PLDI Nicolas Voirol, Etienne Kneuss, Viktor Kuncak
2015	—	`conf`	Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
2015	—	`conf`	Deductive Program Repair. CAV (2) Etienne Kneuss, Manos Koukoutos, Viktor Kuncak
2015	—	`conf`	Developing Verified Software Using Leon. NFM Viktor Kuncak
2015	—	`conf`	InSynth: A System for Code Completion using Types and Weights. Software Engineering & Management Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac
2015	B	`conf`	Induction for SMT Solvers. VMCAI Andrew Reynolds, Viktor Kuncak
2015	—	`conf`	Interactive Synthesis Using Free-Form Queries. ICSE (2) Tihomir Gvero, Viktor Kuncak
2015	J	`jnl`	On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
2015	J	`jnl`	On recursion-free Horn clauses and Craig interpolation. Formal Methods Syst. Des. Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2015	A	`conf`	Programming with enumerable sets of structures. OOPSLA Ivan Kuraj, Viktor Kuncak, Daniel Jackson
2015	—	`conf`	Sound reasoning about integral data types with a reusable SMT solver interface. Scala@PLDI Régis Blanc, Viktor Kuncak
2015	A	`conf`	Synthesizing Java expressions from free-form queries. OOPSLA Tihomir Gvero, Viktor Kuncak
2014	B	`conf`	Checking Data Structure Properties Orders of Magnitude Faster. RV Emmanouil Koukoutos, Viktor Kuncak
2014	J	`jnl`	On Numerical Error Propagation with Sensitivity. CoRR Eva Darulova, Viktor Kuncak
2014	—	`conf`	SciFe: Scala framework for efficient enumeration of data structures with invariants. SCALA@ECOOP Ivan Kuraj, Viktor Kuncak
2014	A*	`conf`	Sound compilation of reals. POPL Eva Darulova, Viktor Kuncak
2014	A*	`conf`	Symbolic Resource Bound Inference for Functional Programs. CAV Ravichandhran Madhavan, Viktor Kuncak
2014	—	`conf`	Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution). ICALP (1) Viktor Kuncak
2013	—	`conf`	An overview of the Leon verification system: verification by translation to recursive functions. SCALA@ECOOP Régis Blanc, Viktor Kuncak, Etienne Kneuss, Philippe Suter
2013	—	`conf`	Automatic synthesis of out-of-core algorithms. SIGMOD Conference Yannis Klonatos, Andres Nötzli, Andrej Spielmann, Christoph Koch, Viktor Kuncak
2013	—	`conf`	Classifying and Solving Horn Clauses for Verification. VSTTE Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2013	A*	`conf`	Complete completion using types and weights. PLDI Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, Ruzica Piskac
2013	J	`jnl`	Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report) CoRR Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2013	A*	`conf`	Disjunctive Interpolants for Horn-Clause Verification. CAV Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2013	—	`conf`	Effect Analysis for Programs with Callbacks. VSTTE Etienne Kneuss, Viktor Kuncak, Philippe Suter
2013	B	`conf`	Executing Specifications Using Synthesis and Constraint Solving. RV Viktor Kuncak, Etienne Kneuss, Philippe Suter
2013	J	`jnl`	Functional synthesis for linear arithmetic and sets. Int. J. Softw. Tools Technol. Transf. Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
2013	—	`conf`	Game programming by demonstration. Onward! Mikaël Mayer, Viktor Kuncak
2013	B	`conf`	Interpolation for synthesis on unbounded domains. FMCAD Viktor Kuncak, Régis Blanc
2013	J	`jnl`	On Integrating Deductive Synthesis and Verification Systems CoRR Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, Philippe Suter
2013	J	`jnl`	On Sound Compilation of Reals. CoRR Eva Darulova, Viktor Kuncak
2013	B	`conf`	Reductions for Synthesis Procedures. VMCAI Swen Jacobs, Viktor Kuncak, Philippe Suter
2013	J	`jnl`	Software verification and graph similarity for automated evaluation of students' assignments. Inf. Softw. Technol. Milena Vujosevic-Janicic, Mladen Nikolic, Dusan Tosic, Viktor Kuncak
2013	A	`conf`	Synthesis modulo recursive functions. OOPSLA Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, Philippe Suter
2013	Misc	`conf`	Synthesis of fixed-point programs. EMSOFT Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha
2013	J	`jnl`	The Relationship between Craig Interpolation and Recursion-Free Horn Clauses CoRR Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2012	B	`conf`	A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer
2012	J	`jnl`	Abortable Linearizable Modules. Arch. Formal Proofs Rachid Guerraoui, Viktor Kuncak, Giuliano Losa
2012	B	`conf`	Accelerating Interpolants. ATVA Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer
2012	B	`conf`	Certifying Solutions for Numerical Constraints. RV Eva Darulova, Viktor Kuncak
2012	A*	`conf`	Constraints as control. POPL Ali Sinan Köksal, Viktor Kuncak, Philippe Suter
2012	—	`conf`	Deciding Functional Lists with Sublist Sets. VSTTE Thomas Wies, Marco Muñiz, Viktor Kuncak
2012	—	`conf`	Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description. VSTTE Milena Vujosevic-Janicic, Viktor Kuncak
2012	J	`jnl`	Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. CoRR Milena Vujosevic-Janicic, Mladen Nikolic, Dusan Tosic, Viktor Kuncak
2012	J	`jnl`	Software synthesis procedures. Commun. ACM Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
2012	A*	`conf`	Speculative linearizability. PLDI Rachid Guerraoui, Viktor Kuncak, Giuliano Losa
2012	A	`conf`	Synthesis for Unbounded Bit-Vector Arithmetic. IJCAR Andrej Spielmann, Viktor Kuncak
2012	B	`ed.`	Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings VMCAI Viktor Kuncak, Andrey Rybalchenko
2011	A	`conf`	An Efficient Decision Procedure for Imperative Tree Data Structures. CADE Thomas Wies, Marco Muñiz, Viktor Kuncak
2011	A*	`conf`	Interactive Synthesis of Code Snippets. CAV Tihomir Gvero, Viktor Kuncak, Ruzica Piskac
2011	B	`conf`	Satisfiability Modulo Recursive Programs. SAS Philippe Suter, Ali Sinan Köksal, Viktor Kuncak
2011	A	`conf`	Scala to the Power of Z3: Integrating SMT and Programming. CADE Ali Sinan Köksal, Viktor Kuncak, Philippe Suter
2011	B	`conf`	Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI Philippe Suter, Robin Steiger, Viktor Kuncak
2011	B	`conf`	Towards Complete Reasoning about Axiomatic Specifications. VMCAI Swen Jacobs, Viktor Kuncak
2011	A	`conf`	Trustworthy numerical computation in Scala. OOPSLA Eva Darulova, Viktor Kuncak
2010	B	`conf`	Building a Calculus of Data Structures. VMCAI Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies
2010	B	`conf`	Collections, Cardinalities, and Relations. VMCAI Kuat Yessenov, Ruzica Piskac, Viktor Kuncak
2010	A*	`conf`	Comfusy: A Tool for Complete Functional Synthesis. CAV Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
2010	A*	`conf`	Complete functional synthesis. PLDI Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
2010	A*	`conf`	Decision procedures for algebraic data types with abstractions. POPL Philippe Suter, Mirco Dotta, Viktor Kuncak
2010	A	`conf`	MUNCH - Automated Reasoner for Sets and Multisets. IJCAR Ruzica Piskac, Viktor Kuncak
2010	B	`conf`	Ordered Sets in the Calculus of Data Structures. CSL Viktor Kuncak, Ruzica Piskac, Philippe Suter
2010	—	`conf`	Phantm: PHP analyzer for type mismatch. SIGSOFT FSE Etienne Kneuss, Philippe Suter, Viktor Kuncak
2010	J	`jnl`	Predicting and preventing inconsistencies in deployed distributed systems. ACM Trans. Comput. Syst. Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak
2010	B	`conf`	Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. RV Etienne Kneuss, Philippe Suter, Viktor Kuncak
2010	B	`conf`	Synthesis for regular specifications over unbounded domains. FMCAD Jad Hamza, Barbara Jobstmann, Viktor Kuncak
2010	—	`conf`	Test generation through programming in UDITA. ICSE (1) Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, Darko Marinov
2009	A*	`conf`	An integrated proof language for imperative programs. PLDI Karen Zee, Viktor Kuncak, Martin C. Rinard
2009	—	`conf`	Combining Theories with Shared Set Operations. FroCoS Thomas Wies, Ruzica Piskac, Viktor Kuncak
2009	Misc	`conf`	CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. NSDI Maysam Yabandeh, Nikola Knezevic, Dejan Kostic, Viktor Kuncak
2009	—	`conf`	Opis: reliable distributed systems in OCaml. TLDI Pierre-Évariste Dagand, Dejan Kostic, Viktor Kuncak
2009	A	`conf`	Simplifying Distributed System Development. HotOS Maysam Yabandeh, Nedeljko Vasic, Dejan Kostic, Viktor Kuncak
2008	B	`conf`	Decision Procedures for Multisets with Cardinality Constraints. VMCAI Ruzica Piskac, Viktor Kuncak
2008	B	`conf`	Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars. CSL Ruzica Piskac, Viktor Kuncak
2008	A*	`conf`	Full functional verification of linked data structures. PLDI Karen Zee, Viktor Kuncak, Martin C. Rinard
2008	A*	`conf`	Linear Arithmetic with Stars. CAV Ruzica Piskac, Viktor Kuncak
2008	B	`conf`	Runtime Checking for Separation Logic. VMCAI Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin
2008	A	`conf`	Verifying linked data structure implementations. IPDPS Karen Zee, Viktor Kuncak, Martin C. Rinard
2007	—	`—`	Modular data structure verification. Viktor Kuncak
2007	B	`conf`	Polynomial Constraints for Sets with Cardinality Bounds. FoSSaCS Bruno Marnette, Viktor Kuncak, Martin C. Rinard
2007	B	`conf`	Runtime Checking for Program Verification. RV Karen Zee, Viktor Kuncak, Michael B. Taylor, Martin C. Rinard
2007	A	`conf`	Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. CADE Viktor Kuncak, Martin C. Rinard
2007	B	`conf`	Using First-Order Theorem Provers in the Jahob Data Structure Verification System. VMCAI Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard
2006	A	`conf`	An overview of the Jahob analysis system: project goals and current status. IPDPS Viktor Kuncak, Martin C. Rinard
2006	J	`jnl`	Deciding Boolean Algebra with Presburger Arithmetic. J. Autom. Reason. Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
2006	B	`conf`	Field Constraint Analysis. VMCAI Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard
2006	J	`jnl`	Modular Pluggable Analyses for Data Structure Consistency. IEEE Trans. Software Eng. Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard
2006	J	`jnl`	On Verifying Complex Properties using Symbolic Shape Analysis CoRR Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, Martin C. Rinard
2005	A	`conf`	An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. CADE Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
2005	—	`conf`	Crosscutting techniques in program specification and analysis. AOSD Patrick Lam, Viktor Kuncak, Martin C. Rinard
2005	—	`conf`	Decision Procedures for Set-Valued Fields. AIOOL@VMCAI Viktor Kuncak, Martin C. Rinard
2005	B	`conf`	Generalized Typestate Checking for Data Structure Consistency. VMCAI Patrick Lam, Viktor Kuncak, Martin C. Rinard
2005	B	`conf`	Hob: A Tool for Verifying Data Structure Consistency. CC Patrick Lam, Viktor Kuncak, Martin C. Rinard
2005	—	`conf`	Implications of a Data Structure Consistency Checking System. VSTTE Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard
2005	J	`jnl`	On Algorithms and Complexity for Sets with Cardinality Constraints CoRR Bruno Marnette, Viktor Kuncak, Martin C. Rinard
2005	—	`conf`	On Algorithms and Complexity for Sets with Cardinality Constraints. Deduction and Applications Viktor Kuncak, Martin C. Rinard, Bruno Marnette
2005	—	`conf`	Relational analysis of algebraic datatypes. ESEC/SIGSOFT FSE Viktor Kuncak, Daniel Jackson
2004	J	`jnl`	Binary Search Trees. Arch. Formal Proofs Viktor Kuncak
2004	B	`conf`	Boolean Algebra of Shape Analysis Constraints. VMCAI Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	File Refinement. Arch. Formal Proofs Karen Zee, Viktor Kuncak
2004	B	`conf`	Generalized Records and Spatial Conjunction in Role Logic. SAS Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	Generalized typestate checking using set interfaces and pluggable analyses. ACM SIGPLAN Notices Patrick Lam, Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	On Generalized Records and Spatial Conjunction in Role Logic CoRR Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	On Role Logic CoRR Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	On Spatial Conjunction as Second-Order Logic CoRR Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	On computing the fixpoint of a set of boolean equations CoRR Viktor Kuncak, K. Rustan M. Leino
2004	J	`jnl`	On the Theory of Structural Subtyping CoRR Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	Roles Are Really Great! CoRR Viktor Kuncak, Patrick Lam, Martin C. Rinard
2004	J	`jnl`	The First-Order Theory of Sets with Cardinality Constraints is Decidable CoRR Viktor Kuncak, Martin C. Rinard
2004	J	`jnl`	Typestate Checking and Regular Graph Constraints CoRR Viktor Kuncak, Martin C. Rinard
2004	C	`conf`	Verifying a File System Implementation. ICFEM Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard
2003	B	`conf`	Existential Heap Abstraction Entailment Is Undecidable. SAS Viktor Kuncak, Martin C. Rinard
2003	A*	`conf`	Structural Subtyping of Non-Recursive Types is Decidable. LICS Viktor Kuncak, Martin C. Rinard
2002	J	`jnl`	Numerical Representations as Purely Functional Data Structures: a New Approach. Informatica Mirjana Ivanovic, Viktor Kuncak
2002	A*	`conf`	Role analysis. POPL Viktor Kuncak, Patrick Lam, Martin C. Rinard
2001	—	`conf`	A Language for Role Specifications. LCPC Viktor Kuncak, Patrick Lam, Martin C. Rinard
2001	—	`conf`	Confluence of Untyped Lambda Calculus via Simple Types. ICTCS Silvia Ghilezan, Viktor Kuncak