vkuncak.bib

@INPROCEEDINGS{SpielmannETAL13AutomaticSynthesisOutCoreAlgorithms,
  author = {Andrej Spielmann and Andres N\"{o}tzli and Christoph Koch and Viktor Kuncak and Yannis Klonatos},
  title = {Automatic Synthesis of Out-of-Core Algorithms},
  booktitle = {SIGMOD},
  year = 2013,
  localurl = {http://lara.epfl.ch/~kuncak/papers/SpielmannETAL13AutomaticSynthesisOutCoreAlgorithms.pdf}
}

@TECHREPORT{BlancETAL13VerificationTranslationRecursiveFunctions,
  author = {R\'egis William Blanc and Etienne Kneuss and Viktor Kuncak and Philippe Suter},
  title = {On Verification by Translation to Recursive Functions},
  institution = {EPFL},
  year = 2013,
  number = {EPFL-REPORT-186233}
}

@TECHREPORT{KneussETAL13IntegratingDeductiveSynthesisVerificationSystems,
  author = {Etienne Kneuss and Viktor Kuncak and Ivan Kuraj and Philippe Suter},
  title = {On Integrating Deductive Synthesis and Verification Systems},
  institution = {EPFL},
  year = 2013,
  number = {EPFL-REPORT-186043}
}

@INPROCEEDINGS{RuemmerETAL13DisjunctiveInterpolantsHornClauseVerification,
  author = {Philipp R\"ummer and Hossein Hojjat and Viktor Kuncak},
  title = {Disjunctive Interpolants for Horn-Clause Verification},
  booktitle = {CAV},
  year = 2013,
  localurl = {http://lara.epfl.ch/~kuncak/papers/RuemmerETAL13DisjunctiveInterpolantsHornClauseVerification.pdf}
}

@INPROCEEDINGS{GveroETAL13CompleteCompletionTypesWeights,
  author = {Tihomir Gvero and Viktor Kuncak and Ivan Kuraj and Ruzica Piskac},
  title = {Complete Completion using Types and Weights},
  booktitle = {PLDI},
  year = 2013,
  localurl = {http://lara.epfl.ch/~kuncak/papers/GveroETAL13CompleteCompletionTypesWeights.pdf}
}

@ARTICLE{Vujosevic-JanicicETAL13SoftwareVerificationGraphSimilarityAutomated,
  author = {Milena Vujo\v{s}evi\'{c}-Jani\v{c}i\'{c} and Mladen Nikoli\'{c} and Du\v{s}an To\v{s}i\'{c} and Viktor Kuncak},
  title = {Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments},
  journal = {Information and Software Technology},
  year = 2013,
  localurl = {http://lara.epfl.ch/~kuncak/papers/Vujosevic-JanicicETAL13SoftwareVerificationGraphSimilarityAutomated.pdf}
}

@INPROCEEDINGS{JacobsETAL13ReductionsSynthesisProcedures,
  author = {Swen Jacobs and Viktor Kuncak and Phillippe Suter},
  title = {Reductions for Synthesis Procedures},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2013,
  localurl = {http://lara.epfl.ch/~kuncak/papers/JacobsETAL13ReductionsSynthesisProcedures.pdf}
}

@INPROCEEDINGS{DarulovaKuncak12CertifyingSolutionsNumericalConstraints,
  author = {Eva Darulova and Viktor Kuncak},
  title = {Certifying Solutions for Numerical Constraints},
  booktitle = {Runtime Verification (RV)},
  year = 2012,
  localurl = {http://lara.epfl.ch/~kuncak/papers/DarulovaKuncak12CertifyingSolutionsNumericalConstraints.pdf}
}

@INPROCEEDINGS{HojjatETAL12AcceleratingInterpolants,
  author = {Hossein Hojjat and Radu Iosif and
  Filip Kone\v{c}n\'{y} and Viktor Kuncak and Philipp R\"ummer},
  title = {Accelerating Interpolants},
  booktitle = {Automated Technology for Verification and Analysis (ATVA)},
  year = 2012,
  localurl = {http://lara.epfl.ch/~kuncak/papers/HojjatETAL12AcceleratingInterpolants.pdf}
}

@INPROCEEDINGS{HojjatETAL12VerificationToolkitNTS,
  author = {Hossein Hojjat and Filip Konecny and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp Ruemmer},
  title = {A Verification Toolkit for Numerical Transition Systems (Tool Paper)},
  booktitle = {16th International Symposium on Formal Methods (FM)},
  year = 2012,
  publisher = {Springer},
  localurl = {http://lara.epfl.ch/~kuncak/papers/HojjatETAL12VerificationToolkitNTS.pdf}
}

@INPROCEEDINGS{SpielmannKuncak12SynthesisUnboundedBitvectorArithmetic,
  author = {Andrej Spielmann and Viktor Kuncak},
  title = {Synthesis for Unbounded Bitvector Arithmetic},
  booktitle = {International Joint Conference on Automated 
Reasoning (IJCAR)},
  year = 2012,
  series = {LNAI},
  publisher = {Springer},
  localurl = {http://lara.epfl.ch/~kuncak/papers/SpielmannKuncak12SynthesisUnboundedBitvectorArithmetic.pdf}
}

@INPROCEEDINGS{GuerraouiETAL12SpeculativeLinearizability,
  author = {Rachid Guerraoui and Viktor Kuncak and Giuliano Losa},
  title = {Speculative Linearizability},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  year = 2012,
  localurl = {http://lara.epfl.ch/~kuncak/papers/GuerraouiETAL12SpeculativeLinearizability.pdf}
}

@ARTICLE{KuncakETAL12SoftwareSynthesisProcedures,
  author = {Viktor Kuncak and Mika\"el Mayer and Ruzica Piskac and Philippe Suter},
  title = {Software Synthesis Procedures},
  journal = {Communications of the ACM},
  date = {February},
  year = 2012,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL12SoftwareSynthesisProcedures.pdf}
}

@ARTICLE{KuncakETAL12FunctionalSynthesisLinearArithmeticSets,
  author = {Viktor Kuncak and Mikael Mayer and Ruzica Piskac and Philippe Suter},
  title = {Functional Synthesis for Linear Arithmetic and Sets},
  journal = {Software Tools for Technology Transfer (STTT)},
  year = 2012,
  volume = {TBD},
  number = {TBD},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL12FunctionalSynthesisLinearArithmeticSets.pdf}
}

@INPROCEEDINGS{WiesETAL12DecidingFunctionalListswithSublistSets,
  author = {Thomas Wies and Marco Mu\~niz and Viktor Kuncak},
  title = {Deciding Functional Lists with Sublist Sets},
  booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
  year = 2012,
  series = {LNCS},
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL12DecidingFunctionalListswithSublistSets.pdf}
}

@INPROCEEDINGS{VujosevicJanicicKuncak12DevelopmentandEvaluationofLAV,
  author = {Milena Vujo\v{s}evi\'{c}-Jani\v{c}i\'{c} and Viktor Kuncak},
  title = {Development and Evaluation of {LAV}: an {SMT}-Based Error Finding Platform},
  booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
  year = 2012,
  series = {LNCS},
  localurl = {http://lara.epfl.ch/~kuncak/papers/VujosevicJanicicKuncak12DevelopmentandEvaluationofLAV.pdf}
}

@INPROCEEDINGS{KoeksalETAL12ConstraintsControl,
  author = {{Ali Sinan} K\"oksal and Viktor Kuncak and Philippe Suter},
  title = {Constraints as Control},
  booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
  year = 2012,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KoeksalETAL12ConstraintsControl.pdf}
}

@INPROCEEDINGS{DarulovaKuncak11TrustworthyNumericalComputationinScala,
  author = {Eva Darulov\'a and Viktor Kuncak},
  title = {Trustworthy Numerical Computation in Scala},
  booktitle = {OOPSLA},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/DarulovaKuncak11TrustworthyNumericalComputationinScala.pdf}
}

@INPROCEEDINGS{SuterETAL11SatisfiabilityModuloRecursivePrograms,
  author = {Philippe Suter and Ali Sinan K\"{o}ksal and Viktor Kuncak},
  title = {Satisfiability Modulo Recursive Programs},
  booktitle = {Static Analysis Symposium (SAS)},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf}
}

@INPROCEEDINGS{WiesETAL11EfficientDecisionProcedureforImperative,
  author = {Thomas Wies and Marco {Mu\~{n}iz} and Viktor Kuncak},
  title = {An Efficient Decision Procedure for Imperative Tree Data Structures},
  booktitle = {Computer-Aideded Deduction (CADE)},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL11EfficientDecisionProcedureforImperative.pdf}
}

@INPROCEEDINGS{KoeksalETAL11ScalaZ3,
  author = {{Ali Sinan} K{\"o}ksal and Viktor Kuncak and Philippe Suter},
  title = {Scala to the Power of {Z3}: Integrating {SMT} and Programming},
  booktitle = {Computer-Aideded Deduction (CADE) Tool Demo},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KoeksalETAL11ScalaZ3.pdf}
}

@INPROCEEDINGS{GveroETAL11InteractiveSynthesisofCodeSnippets,
  author = {Tihomir Gvero and Viktor Kuncak and Ruzica Piskac},
  title = {Interactive Synthesis of Code Snippets},
  booktitle = {Computer Aided Verification (CAV) Tool Demo},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/GveroETAL11InteractiveSynthesisofCodeSnippets.pdf}
}

@INPROCEEDINGS{SuterETAL11SetswithCardinalityConstraintsin,
  author = {Philippe Suter and Robin Steiger and Viktor Kuncak},
  title = {Sets with Cardinality Constraints in Satisfiability Modulo Theories},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/SuterETAL11SetswithCardinalityConstraintsin.pdf}
}

@INPROCEEDINGS{JacobsKuncak11TowardsCompleteReasoningaboutAxiomaticSpecifications,
  author = {Swen Jacobs and Viktor Kuncak},
  title = {Towards Complete Reasoning about Axiomatic Specifications},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2011,
  localurl = {http://lara.epfl.ch/~kuncak/papers/JacobsKuncak11TowardsCompleteReasoningaboutAxiomaticSpecifications.pdf}
}

@TECHREPORT{SuterETAL10OnSatisfiabilityModuloComputableFunctions,
  author = {Philippe Suter and Ali Sinan K\"oksal and Viktor Kuncak},
  title = {On Satisfiability Modulo Computable Functions},
  institution = {EPFL},
  number = {EPFL-REPORT},
  year = 2010
}

@TECHREPORT{DarulovaKuncak10OnRigorousNumericalComputationasScalaLibrary,
  author = {Eva Darulova and Viktor Kuncak},
  title = {On Rigorous Numerical Computation as a Scala Library},
  institution = {EPFL},
  year = 2010,
  number = {EPFL-REPORT-158754}
}

@INPROCEEDINGS{KneussETAL10Phantm,
  author = {Etienne Kneuss and Philippe Suter and Viktor Kuncak},
  title = {{Phantm}: {PHP} Analyzer for Type Mismatch (Research Demonstration)},
  booktitle = {ACM SIGSOFT Conference on Foundations of Software Engineering (FSE)},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KneussETAL10Phantm.pdf}
}

@INPROCEEDINGS{KneussETAL10RuntimeInstrumentationforPreciseFlow,
  author = {Etienne Kneuss and Philippe Suter and Viktor Kuncak},
  title = {Runtime Instrumentation for Precise Flow-Sensitive Type Analysis},
  booktitle = {International Conference on Runtime Verification},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KneussETAL10RuntimeInstrumentationforPreciseFlow.pdf}
}

@INPROCEEDINGS{HamzaETAL10SynthesisforRegularSpecificationsoverUnboundedDomains,
  author = {Jad Hamza and Barbara Jobstmann and Viktor Kuncak},
  title = {Synthesis for Regular Specifications over Unbounded Domains},
  booktitle = {FMCAD},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/HamzaETAL10SynthesisforRegularSpecificationsoverUnboundedDomains.pdf}
}

@INPROCEEDINGS{KuncakETAL10OrderedSetsinCalculusofDataStructures,
  author = {Viktor Kuncak and Ruzica Piskac and Philippe Suter},
  title = {Ordered Sets in the Calculus of Data Structures (Invited Paper)},
  booktitle = {CSL},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL10OrderedSetsinCalculusofDataStructures.pdf}
}

@TECHREPORT{WiesETAL10DecidingFunctionalListswithSublistSets,
  author = {Thomas Wies and Marco Mu\~niz and Viktor Kuncak},
  title = {On Deciding Functional Lists with Sublist Sets},
  institution = {EPFL},
  year = 2010,
  number = {EPFL-REPORT-148361},
  month = {April},
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL10DecidingFunctionalListswithSublistSets.pdf}
}

@TECHREPORT{JacobsKuncak10LocalityofOneVariableAxioms,
  author = {Swen Jacobs and Kuncak, Viktor},
  title = {On Locality of One-Variable Axioms and Piecewise Combinations},
  institution = {EPFL},
  year = 2010,
  number = {EPFL-REPORT-148180},
  month = {April},
  localurl = {http://lara.epfl.ch/~kuncak/papers/JacobsKuncak10LocalityofOneVariableAxioms.pdf}
}

@INPROCEEDINGS{PiskacKuncak10MUNCHAutomatedReasonerforSets,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {MUNCH - Automated Reasoner for Sets and Multisets (System Description)},
  booktitle = {IJCAR},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak10MUNCHAutomatedReasonerforSets.pdf}
}

@INPROCEEDINGS{KuncakETAL10Comfusy,
  author = {Viktor Kuncak and Mikael Mayer and  Ruzica Piskac and Philippe Suter},
  title = {Comfusy: Complete Functional Synthesis (Tool Presentation)},
  booktitle = {CAV},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL10Comfusy.pdf}
}

@INPROCEEDINGS{KuncakETAL10CompleteFunctionalSynthesis,
  author = {Viktor Kuncak and Mikael Mayer and Ruzica Piskac and Philippe Suter},
  title = {Complete Functional Synthesis},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL10CompleteFunctionalSynthesis.pdf}
}

@TECHREPORT{PiskacETAL10DecisionProceduresforOrderedCollections,
  author = {Ruzica Piskac and Philippe Suter and Viktor Kuncak},
  title = {On Decision Procedures for Ordered Collections},
  institution = {EPFL},
  year = 2010,
  number = {LARA-REPORT-2010-001},
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacETAL10DecisionProceduresforOrderedCollections.pdf}
}

@INPROCEEDINGS{GligoricETAL10TestGenerationthroughProgramminginUDITA,
  author = {Milos Gligoric and Tihomir Gvero and Vilas Jagannath and Sarfraz Khurshid and Viktor Kuncak and Darko Marinov},
  booktitle = {International Conference on Software Engineering (ICSE)},
  title = {Test Generation through Programming in {UDITA}},
  url = {http://mir.cs.uiuc.edu/udita},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/GligoricETAL10TestGenerationthroughProgramminginUDITA.pdf}
}

@ARTICLE{YabandehETAL10PredictingandpreventingInconsistencies,
  author = {Maysam Yabandeh and Nikola Kne\v{z}evi\'c and Dejan Kosti\'c and Viktor Kuncak},
  title = {Predicting and Preventing Inconsistencies in Deployed Distributed Systems},
  journal = {ACM Transactions on Computer Systems},
  year = 2010,
  volume = {28},
  number = 1,
  localurl = {http://lara.epfl.ch/~kuncak/papers/YabandehETAL10PredictingandpreventingInconsistencies.pdf}
}

@INPROCEEDINGS{KuncakETAL10Building,
  author = {Viktor Kuncak and Ruzica Piskac and Philippe Suter and Thomas Wies},
  title = {Building a Calculus of Data Structures (invited paper)},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL10Building.pdf}
}

@INPROCEEDINGS{YessenovETAL10CollectionsRelations,
  author = {Kuat Yessenov and Ruzica Piskac and Viktor Kuncak},
  title = {Collections, Cardinalities, and Relations},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2010,
  localurl = {http://lara.epfl.ch/~kuncak/papers/YessenovETAL10CollectionsRelations.pdf}
}

@INPROCEEDINGS{SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions,
  author = {Philippe Suter and Mirco Dotta and Viktor Kuncak},
  title = {Decision Procedures for Algebraic Data Types with Abstractions},
  year = 2010,
  booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
  localurl = {http://lara.epfl.ch/~kuncak/papers/SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions.pdf}
}

@TECHREPORT{SuterETAL09CompleteFunctionalSynthesis,
  author = {Philippe Suter and Ruzica Piskac and Mikael Mayer and Viktor Kuncak},
  title = {On Complete Functional Synthesis},
  institution = {EPFL},
  year = 2009,
  number = {LARA-REPORT-2009-006},
  localurl = {http://lara.epfl.ch/~kuncak/papers/SuterETAL09CompleteFunctionalSynthesis.pdf}
}

@TECHREPORT{GligoricETAL09TestGenerationthroughProgramminginUDITA,
  author = {Milos Gligoric and Tihomir Gvero and Vilas Jagannath and Sarfraz Khurshid and Viktor Kuncak and Darko Marinov},
  title = {On Test Generation through Programming in {UDITA}},
  institution = {EPFL, IC},
  number = {LARA-REPORT-2009-05},
  month = {September},
  url = {http://mir.cs.uiuc.edu/udita},
  year = 2009,
  localurl = {http://lara.epfl.ch/~kuncak/papers/GligoricETAL09TestGenerationthroughProgramminginUDITA.pdf}
}

@TECHREPORT{YessenovETAL09OnDecisionProceduresCollectionsRelations,
  author = {Kuat Yessenov and Viktor Kuncak and Ruzica Piskac},
  title = {On Decision Procedures for Collections, Cardinalities, and Relations},
  institution = {EPFL},
  year = 2009,
  number = {LARA-REPORT-2009-004},
  month = {29 August},
  localurl = {http://lara.epfl.ch/~kuncak/papers/YessenovETAL09OnDecisionProceduresCollectionsRelations.pdf}
}

@TECHREPORT{SuterETAL09DecisionProceduresforAlgebraicData,
  author = {Philippe Suter and Mirco Dotta and Viktor Kuncak},
  title = {On Decision Procedures for Algebraic Data Types with Abstractions},
  institution = {EPFL},
  year = 2009,
  number = {LARA-REPORT-2009-003},
  month = {16 July},
  localurl = {http://lara.epfl.ch/~kuncak/papers/SuterETAL09DecisionProceduresforAlgebraicData.pdf}
}

@INPROCEEDINGS{WiesETAL09CombiningTheorieswithSharedSetOperations,
  author = {Thomas Wies and Ruzica Piskac and Viktor Kuncak},
  title = {Combining Theories with Shared Set Operations},
  booktitle = {FroCoS: Frontiers in Combining Systems},
  year = 2009,
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.pdf}
}

@TECHREPORT{WiesETAL09OnCombiningTheorieswithSharedSetOperations,
  author = {Thomas Wies and Ruzica Piskac and Viktor Kuncak},
  title = {On Combining Theories with Shared Set Operations},
  institution = {EPFL},
  number = {LARA-REPORT-2009-002},
  year = 2009,
  month = {May 9},
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL09OnCombiningTheorieswithSharedSetOperations.pdf}
}

@INPROCEEDINGS{YabandehETAL09SimplifyingDistributedSystemHotOS,
  author = {Maysam Yabandeh and Nedeljko Vasi\'c and Dejan Kosti\'c and Viktor  Kuncak},
  title = {Simplifying Distributed System Development},
  year = 2009,
  booktitle = {12th Workshop on Hot Topics in Operating Systems},
  localurl = {http://lara.epfl.ch/~kuncak/papers/YabandehETAL09SimplifyingDistributedSystemHotOS.pdf}
}

@INPROCEEDINGS{ZeeETAL09IntegratedProofLanguageforImperativePrograms,
  author = {Karen Zee and Viktor Kuncak and Martin Rinard},
  title = {An Integrated Proof Language for Imperative Programs},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  year = 2009,
  localurl = {http://lara.epfl.ch/~kuncak/papers/ZeeETAL09IntegratedProofLanguageforImperativePrograms.pdf}
}

@TECHREPORT{KuncakWies09SetDrivenCombinationofLogicsandVerifiers,
  author = {Viktor Kuncak and Thomas Wies},
  title = {On Set-Driven Combination of Logics and Verifiers},
  institution = {EPFL},
  year = 2009,
  month = {February},
  number = {LARA-REPORT-2009-001},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakWies09SetDrivenCombinationofLogicsandVerifiers.pdf}
}

@TECHREPORT{YabandehETAL09SimplifyingDistributedSystemDevelopment,
  author = {Maysam Yabandeh and Nedeljko Vasi\'c and Dejan Kosti\'c and Viktor  Kuncak},
  title = {Simplifying Distributed System Development},
  institution = {EPFL},
  year = 2009,
  number = {NSL-REPORT-2009-001},
  localurl = {http://lara.epfl.ch/~kuncak/papers/YabandehETAL09SimplifyingDistributedSystemDevelopment.pdf}
}

@INPROCEEDINGS{YabandehETAL09CrystalBall,
  author = {Maysam Yabandeh and Nikola Kne\v{z}evi\'c and Dejan Kosti\'c and Viktor Kuncak},
  title = {{CrystalBall}: Predicting and Preventing Inconsistencies in Deployed Distributed Systems},
  year = 2009,
  booktitle = {6th USENIX Symp. Networked Systems Design and Implementation (NSDI '09)},
  url = {http://www.usenix.org/events/nsdi09/tech/full_papers/yabandeh/yabandeh_html/index.html},
  localurl = {http://lara.epfl.ch/~kuncak/papers/YabandehETAL09CrystalBall.pdf}
}

@INPROCEEDINGS{DagandETAL09Opis,
  author = {Pierre-\'Evariste Dagand and Dejan Kosti\'c and Viktor Kuncak},
  title = {Opis: Reliable Distributed Systems in {OCaml}},
  booktitle = {ACM SIGPLAN TLDI},
  year = 2009,
  localurl = {http://lara.epfl.ch/~kuncak/papers/DagandETAL09Opis.pdf}
}

@TECHREPORT{GligoricETAL08OnDelayedChoiceExecutionforFalsification,
  author = {Milos Gligoric and Tihomir Gvero and Sarfraz Khurshid and Viktor Kuncak and Darko Marinov},
  title = {On Delayed Choice Execution for Falsification},
  institution = {EPFL, IC},
  number = {LARA-REPORT-2008-08},
  year = 2008,
  localurl = {http://lara.epfl.ch/~kuncak/papers/GligoricETAL08OnDelayedChoiceExecutionforFalsification.pdf}
}

@TECHREPORT{Kuncak08ConstraintSolvingforSoftwareReliability,
  author = {Viktor Kuncak},
  title = {Constraint Solving for Software Reliability and Text Analysis (Research Plan)},
  institution = {EPFL},
  year = 2008,
  number = {LARA-REPORT-2008-007},
  month = {August}
}

@TECHREPORT{DagandETAL08Opis,
  author = {Pierre-\'Evariste Dagand and Dejan Kosti\'c and Viktor Kuncak},
  title = {Opis: Reliable Distributed Systems in {OCaml}},
  institution = {EPFL-IC-NSL},
  year = 2008,
  number = {NSL-REPORT-2008-001},
  localurl = {http://lara.epfl.ch/~kuncak/papers/DagandETAL08Opis.pdf}
}

@TECHREPORT{YabandehETAL08CrystalBall,
  author = {Maysam Yabandeh and Nikola Kne\v{z}evi\'c and Dejan Kosti\'c and Viktor Kuncak},
  title = {{CrystalBall}: Predicting and Preventing Inconsistencies in Deployed Distributed Systems},
  institution = {EPFL-IC-LARA},
  year = 2008,
  number = {LARA-REPORT-2008-006},
  month = {May},
  localurl = {http://lara.epfl.ch/~kuncak/papers/YabandehETAL08CrystalBall.pdf}
}

@INPROCEEDINGS{PiskacKuncak08FractionalCollections,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Fractional Collections with Cardinality Bounds, 
and Mixed Integer Linear Arithmetic with Stars},
  booktitle = {Computer Science Logic (CSL)},
  year = 2008,
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08FractionalCollections.pdf}
}

@INPROCEEDINGS{PiskacKuncak08LinearArithmeticwithStars,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Linear Arithmetic with Stars},
  booktitle = {Computed-Aided Verification (CAV)},
  year = 2008,
  series = {LNCS},
  volume = {5123},
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08LinearArithmeticwithStars.pdf}
}

@INPROCEEDINGS{ZeeETAL08FullFunctionalVerificationofLinkedDataStructures,
  title = {Full Functional Verification of Linked Data Structures},
  author = {Karen Zee and Viktor Kuncak and Martin Rinard},
  booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation  (PLDI)},
  note = {see also \cite{Kuncak07DecisionProceduresModularDataStructureVerification}},
  year = 2008,
  localurl = {http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.pdf}
}

@TECHREPORT{PiskacKuncak08OnLinearArithmeticwithStars,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {On Linear Arithmetic with Stars},
  institution = {EPFL},
  number = {LARA-REPORT-2008-005},
  year = 2008,
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08OnLinearArithmeticwithStars.pdf}
}

@TECHREPORT{DottaETAL08OnStaticAnalysisExpressivePatternMatching,
  author = {Mirco Dotta and Philippe Suter and Viktor Kuncak},
  title = {On Static Analysis for Expressive Pattern Matching},
  institution = {EPFL},
  year = 2008,
  number = {LARA-REPORT-2008-004},
  localurl = {http://lara.epfl.ch/~kuncak/papers/DottaETAL08OnStaticAnalysisExpressivePatternMatching.pdf}
}

@INPROCEEDINGS{PiskacKuncak08DecisionProceduresMultisetsCardinality,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Decision Procedures for Multisets with Cardinality Constraints},
  booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  series = {LNCS},
  year = 2008,
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08DecisionProceduresMultisetsCardinality.pdf}
}

@INPROCEEDINGS{NguyenETAL08RuntimeCheckingSeparationLogic,
  author = {Huu Hai Nguyen and Viktor Kuncak and Wei Ngan Chin},
  title = {Runtime Checking for Separation Logic},
  booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  series = {LNCS},
  year = 2008,
  localurl = {http://lara.epfl.ch/~kuncak/papers/NguyenETAL08RuntimeCheckingSeparationLogic.pdf}
}

@TECHREPORT{PiskacKuncak07MultisetsCardinality,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Decision Procedures for Multisets with 
Cardinality Constraints},
  year = 2007,
  number = {LARA-REPORT-2007-002},
  institution = {EPFL},
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak07MultisetsCardinality.pdf}
}

@TECHREPORT{NguyenETAL07RuntimeCheckingforSeparationLogic,
  author = {Huu Hai Nguyen and Viktor Kuncak and Wei Ngan Chin},
  title = {Runtime Checking for Separation Logic},
  institution = {EPFL},
  year = 2007,
  number = {LARA-REPORT-2007-003},
  localurl = {http://lara.epfl.ch/~kuncak/papers/NguyenETAL07RuntimeCheckingforSeparationLogic.pdf}
}

@INPROCEEDINGS{KuncakRinard07TowardsEfficientSatisfiabilityCheckingBoolean,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Towards Efficient Satisfiability Checking for
{B}oolean {A}lgebra with {P}resburger {A}rithmetic},
  booktitle = {Conference on Automateded Deduction (CADE-21)},
  series = {LNCS},
  volume = {4603},
  year = 2007,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard07TowardsEfficientSatisfiabilityCheckingBoolean.pdf}
}

@INPROCEEDINGS{MarnetteETAL07PolynomialConstraintsSetsCardinalityBounds,
  author = {Bruno Marnette and Viktor Kuncak and Martin Rinard},
  title = {Polynomial Constraints for Sets with Cardinality Bounds},
  booktitle = {Foundations of Software Science and Computation Structures (FOSSACS)},
  series = {LNCS},
  volume = {4423},
  year = 2007,
  month = {March},
  localurl = {http://lara.epfl.ch/~kuncak/papers/MarnetteETAL07PolynomialConstraintsSetsCardinalityBounds.pdf}
}

@INPROCEEDINGS{WiesETAL07VerifyingComplexPropertiesSymbolicShapeAnalysis,
  author = {Thomas Wies and Viktor Kuncak and Karen Zee and
Andreas Podelski and Martin Rinard},
  title = {Verifying Complex Properties using Symbolic Shape Analysis},
  booktitle = {Workshop on Heap Abstraction and Verification 
(collocated with ETAPS)},
  year = 2007,
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL07VerifyingComplexPropertiesSymbolicShapeAnalysis.pdf}
}

@INPROCEEDINGS{ZeeETAL07RuntimeCheckingProgramVerification,
  author = {Karen Zee and Viktor Kuncak and Michael Taylor 
and Martin Rinard},
  title = {Runtime Checking for Program Verification},
  booktitle = {Workshop on Runtime Verification},
  series = {LNCS},
  volume = {4839},
  year = 2007,
  localurl = {http://lara.epfl.ch/~kuncak/papers/ZeeETAL07RuntimeCheckingProgramVerification.pdf}
}

@PHDTHESIS{Kuncak07DecisionProceduresModularDataStructureVerification,
  author = {Viktor Kuncak},
  title = {Modular Data Structure Verification},
  school = {EECS Department, Massachusetts Institute of Technology},
  month = {February},
  year = {2007},
  url = {http://hdl.handle.net/1721.1/38533},
  localurl = {http://lara.epfl.ch/~kuncak/papers/Kuncak07DecisionProceduresModularDataStructureVerification.pdf}
}

@TECHREPORT{Kuncak07QuantifierFreeBAPAinNP,
  author = {Viktor Kuncak},
  title = {Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete},
  institution = {MIT CSAIL},
  year = 2007,
  month = {January},
  url = {http://hdl.handle.net/1721.1/35258},
  number = {MIT-CSAIL-TR-2007-001},
  localurl = {http://lara.epfl.ch/~kuncak/papers/Kuncak07QuantifierFreeBAPAinNP.pdf}
}

@INPROCEEDINGS{BouillaguetETAL07UsingFirstOrderTheoremProvers,
  author = {Charles Bouillaguet and Viktor Kuncak and Thomas Wies and Karen Zee and Martin Rinard},
  title = {Using First-Order Theorem Provers in the {J}ahob Data Structure Verification System},
  booktitle = {Verification, Model Checking and Abstract Interpretation},
  year = 2007,
  series = {LNCS},
  volume = {4349},
  month = {November},
  note = {See \cite{BouillaguetETAL06UsingFirstOrderTheoremProvers} for full version},
  localurl = {http://lara.epfl.ch/~kuncak/papers/BouillaguetETAL07UsingFirstOrderTheoremProvers.pdf}
}

@TECHREPORT{BouillaguetETAL06UsingFirstOrderTheoremProvers,
  author = {Charles Bouillaguet and Viktor Kuncak and Thomas Wies and Karen Zee and Martin Rinard},
  title = {On Using First-Order Theorem Provers in a the {J}ahob Data Structure Verification System},
  institution = {MIT},
  number = {MIT-CSAIL-TR-2006-072},
  year = 2006,
  url = {http://hdl.handle.net/1721.1/34874},
  month = {November},
  note = {Full version of \cite{BouillaguetETAL07UsingFirstOrderTheoremProvers}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/BouillaguetETAL06UsingFirstOrderTheoremProvers.pdf}
}

@ARTICLE{KuncakETAL06ModularPluggableAnalysesDataStructureConsistency,
  author = {Viktor Kuncak and Patrick Lam and Karen Zee and Martin Rinard},
  title = {Modular Pluggable Analyses for Data Structure Consistency},
  journal = {IEEE Transactions on Software Engineering (TSE)},
  volume = 32,
  number = 12,
  month = {December},
  year = 2006,
  url = {http://dx.doi.org/10.1109/TSE.2006.125},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL06ModularPluggableAnalysesDataStructureConsistency.pdf}
}

@TECHREPORT{WiesETAL06VerifyingComplexPropertiesSymbolicShapeAnalysis,
  author = {Thomas Wies and Viktor Kuncak and Karen Zee and Andreas Podelski and Martin Rinard},
  title = {On Verifying Complex Properties using Symbolic Shape Analysis},
  institution = {Max-Planck Institute for Computer Science},
  year = 2006,
  number = {MPI-I-2006-2-1},
  url = {http://arxiv.org/abs/cs.PL/0609104},
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL06VerifyingComplexPropertiesSymbolicShapeAnalysis.pdf}
}

@ARTICLE{KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic,
  author = {Viktor Kuncak and Huu Hai Nguyen and Martin Rinard},
  title = {Deciding {B}oolean {A}lgebra with {P}resburger {A}rithmetic},
  journal = {Journal of Automated Reasoning},
  year = 2006,
  volume = {36},
  number = 3,
  url = {http://dx.doi.org/10.1007/s10817-006-9042-1},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf}
}

@INPROCEEDINGS{KuncakRinard06OverviewJahobAnalysisSystem,
  author = {Viktor Kuncak and Martin Rinard},
  title = {An overview of the {J}ahob analysis system: Project Goals and Current Status},
  booktitle = {{NSF} Next Generation Software Workshop},
  year = {2006},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard06OverviewJahobAnalysisSystem.pdf}
}

@INPROCEEDINGS{WiesETAL06FieldConstraintAnalysis,
  author = {Thomas Wies and Viktor Kuncak and Patrick Lam and Andreas Podelski and Martin Rinard},
  title = {Field Constraint Analysis},
  booktitle = {Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation},
  series = {LNCS},
  volume = {3855},
  year = 2006,
  note = {See \cite{WiesETAL05OnFieldConstraintAnalysis} for full version.},
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL06FieldConstraintAnalysis.pdf}
}

@TECHREPORT{WiesETAL05OnFieldConstraintAnalysis,
  author = {Thomas Wies and Viktor Kuncak and Patrick Lam and Andreas Podelski and Martin Rinard},
  title = {On Field Constraint Analysis},
  institution = {MIT CSAIL},
  year = 2005,
  month = {November},
  number = {MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010},
  note = {Full version of \cite{WiesETAL06FieldConstraintAnalysis}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL05OnFieldConstraintAnalysis.pdf}
}

@INPROCEEDINGS{KuncakETAL05ImplicationsDataStructureConsistencyCheckingSystem,
  author = {Viktor Kuncak and Patrick Lam and Karen Zee and Martin Rinard},
  title = {Implications of a Data Structure Consistency Checking System},
  booktitle = {International conference on Verified Software: Theories, Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference)},
  year = 2005,
  address = {Z\"urich, Switzerland},
  month = {10--13th October},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL05ImplicationsDataStructureConsistencyCheckingSystem.pdf}
}

@INPROCEEDINGS{KuncakJackson05RelationalAnalysisAlgebraicDatatypes,
  author = {Viktor Kuncak and Daniel Jackson},
  title = {Relational Analysis of Algebraic Datatypes},
  booktitle = {10th European Soft. Eng. Conf. (ESEC) and 13th
                  Symp. Foundations of Software Engineering (FSE)},
  year = 2005,
  note = {See \cite{KuncakJackson05OnRelationalAnalysisAlgebraicDatatypes}
          for full version.},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakJackson05RelationalAnalysisAlgebraicDatatypes.pdf}
}

@TECHREPORT{MarnetteETAL05AlgorithmsComplexitySetsCardinalityConstraints,
  author = {Bruno Marnette and Viktor Kuncak and Martin Rinard},
  title = {On Algorithms and Complexity for Sets with Cardinality Constraints},
  institution = {MIT CSAIL},
  year = 2005,
  month = {August},
  url = {http://arxiv.org/abs/cs/0508123},
  localurl = {http://lara.epfl.ch/~kuncak/papers/MarnetteETAL05AlgorithmsComplexitySetsCardinalityConstraints.pdf}
}

@INPROCEEDINGS{KuncakETAL05AlgorithmDecidingBAPA,
  author = {Viktor Kuncak and Huu Hai Nguyen and Martin Rinard},
  title = {An Algorithm for Deciding {BAPA}: {B}oolean {A}lgebra with {P}resburger {A}rithmetic},
  booktitle = {20th International Conference on Automated Deduction, CADE-20},
  year = 2005,
  address = {Tallinn, Estonia},
  series = {LNCS},
  volume = {3632},
  month = {July},
  note = {Superseded by 
          \cite{KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL05AlgorithmDecidingBAPA.pdf}
}

@TECHREPORT{KuncakJackson05OnRelationalAnalysisAlgebraicDatatypes,
  author = {Viktor Kuncak and Daniel Jackson},
  title = {On Relational Analysis of Algebraic Datatypes},
  institution = {MIT},
  year = 2005,
  number = 985,
  month = {April},
  note = {Full version of 
          \cite{KuncakJackson05RelationalAnalysisAlgebraicDatatypes}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakJackson05OnRelationalAnalysisAlgebraicDatatypes.pdf}
}

@INPROCEEDINGS{LamETAL05HobTool,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Hob: A Tool for Verifying Data Structure Consistency},
  booktitle = {14th International Conference on Compiler Construction 
                  (tool demo)},
  year = 2005,
  series = {LNCS},
  volume = {3443},
  month = {April},
  localurl = {http://lara.epfl.ch/~kuncak/papers/LamETAL05HobTool.pdf}
}

@INPROCEEDINGS{LamETAL05CrossCuttingTechniquesProgramSpecificationAnalysis,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Cross-Cutting Techniques in Program Specification and Analysis},
  booktitle = {4th International Conference on 
                  Aspect-Oriented Software Development},
  publisher = {ACM},
  isbn = {1-59593-042-6},
  month = {March},
  year = 2005,
  localurl = {http://lara.epfl.ch/~kuncak/papers/LamETAL05CrossCuttingTechniquesProgramSpecificationAnalysis.pdf}
}

@ARTICLE{KuncakRinard05DecisionProceduresSetValuedFields,
  author = {Viktor Kuncak and
               Martin C. Rinard},
  title = {Decision Procedures for Set-Valued Fields},
  journal = {Electr. Notes Theor. Comput. Sci.; Proc. Abstract Interpretation of 
                  Object-Oriented Languages},
  volume = {131},
  year = {2005},
  note = {See \cite{KuncakRinard04DecisionProcedureSetValuedFields} 
          for full version},
  pages = {51-62},
  ee = {http://dx.doi.org/10.1016/j.entcs.2005.01.022},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard05DecisionProceduresSetValuedFields.pdf}
}

@INPROCEEDINGS{LamETAL05GeneralizedTypestateCheckingDataStructureConsistency,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Generalized Typestate Checking for Data Structure Consistency},
  booktitle = {Verification, Model Checking and Abstract Interpretation},
  series = {LNCS},
  volume = {3385},
  year = 2005,
  localurl = {http://lara.epfl.ch/~kuncak/papers/LamETAL05GeneralizedTypestateCheckingDataStructureConsistency.pdf}
}

@MISC{ZeeKuncak04FileRefinement,
  author = {Karen Zee and Viktor Kuncak},
  title = {File Refinement},
  howpublished = {The Archive of Formal Proofs},
  url = {http://afp.sourceforge.net/entries/FileRefinement.shtml},
  month = {December},
  note = {Formal proof development},
  year = 2004
}

@MISC{Kuncak04BinarySearchTrees,
  author = {Viktor Kuncak},
  title = {Binary Search Trees},
  howpublished = {The Archive of Formal Proofs},
  url = {http://afp.sourceforge.net/entries/BinarySearchTree.shtml},
  month = {April},
  note = {Formal proof development},
  year = 2004
}

@INPROCEEDINGS{KuncakETAL04ModularPluggableAnalysesDataStructureConsistency,
  author = {Viktor Kuncak and Patrick Lam and Karen Zee and Martin Rinard},
  title = {Modular Pluggable Analyses for Data Structure Consistency},
  booktitle = {Monterey Workshop on Software Engineering Tools: Compatibility and Integration},
  year = 2004,
  address = {Vienna, Austria},
  month = {October},
  note = {Superseded by 
          \cite{KuncakETAL07ModularPluggableAnalysesDataStructureConsistency}}
}

@TECHREPORT{KuncakRinard04DecisionProcedureSetValuedFields,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On Decision Procedures for Set-Valued Fields},
  institution = {MIT CSAIL},
  year = 2004,
  number = {975},
  month = {November},
  note = {Full version of \cite{KuncakRinard05DecisionProceduresSetValuedFields}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04DecisionProcedureSetValuedFields.pdf}
}

@INPROCEEDINGS{ZeeETAL04CombiningTheoremStaticAnalysisDataStructureConsistency,
  author = {Karen Zee and Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Combining Theorem proving with Static Analysis for Data Structure Consistency},
  booktitle = {International Workshop on Software Verification and Validation},
  year = 2004,
  address = {Seattle},
  month = {November},
  localurl = {http://lara.epfl.ch/~kuncak/papers/ZeeETAL04CombiningTheoremStaticAnalysisDataStructureConsistency.pdf}
}

@TECHREPORT{KuncakRinard04SpatialConjunctionSecondOrderLogic,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On Spatial Conjunction as Second-Order Logic},
  institution = {MIT CSAIL},
  year = 2004,
  number = {970},
  month = {October},
  url = {http://arxiv.org/abs/cs.LO/0410073},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04SpatialConjunctionSecondOrderLogic.pdf}
}

@TECHREPORT{LamETAL04OurExperienceModularPluggableAnalyses,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {On Our Experience with Modular Pluggable Analyses},
  institution = {MIT CSAIL},
  month = {September},
  number = {965},
  year = 2004,
  localurl = {http://lara.epfl.ch/~kuncak/papers/LamETAL04OurExperienceModularPluggableAnalyses.pdf}
}

@TECHREPORT{KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable,
  author = {Viktor Kuncak and Martin Rinard},
  title = {The First-Order Theory of Sets with Cardinality Constraints is Decidable},
  institution = {MIT CSAIL},
  year = 2004,
  number = 958,
  month = {July},
  url = {http://arxiv.org/abs/cs/0407045},
  note = {Superseded by 
          \cite{KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable.pdf}
}

@INPROCEEDINGS{ArkoudasETAL04VerifyingFileSystemImplementationICFEM,
  author = {Konstantine Arkoudas and Karen Zee and Viktor Kuncak and Martin Rinard},
  title = {Verifying a File System Implementation},
  booktitle = {Sixth International Conference on Formal Engineering Methods},
  year = 2004,
  address = {Seattle},
  series = {LNCS},
  volume = {3308},
  month = {Nov 8-12, 2004},
  note = {See also technical report
          \cite{ArkoudasETAL04VerifyingFileSystemImplementationICFEM}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/ArkoudasETAL04VerifyingFileSystemImplementationICFEM.pdf}
}

@INPROCEEDINGS{KuncakRinard04GeneralizedRecordsRoleLogic,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Generalized Records and Spatial Conjunction in Role Logic},
  booktitle = {International Static Analysis Symposium},
  year = 2004,
  address = {Verona, Italy},
  series = {LNCS},
  volume = {3148},
  month = {August 26--28},
  note = {See \cite{KuncakRinard04OnRecordsSpatialConjunctionRoleLogic} for
          full version},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04GeneralizedRecordsRoleLogic.pdf}
}

@TECHREPORT{KuncakRinard04OnRecordsSpatialConjunctionRoleLogic,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On Generalized Records and Spatial Conjunction in Role Logic},
  institution = {MIT CSAIL},
  number = {942},
  year = 2004,
  month = {April},
  url = {http://arxiv.org/abs/cs.PL/0408019},
  note = {Full version of \cite{KuncakRinard04GeneralizedRecordsRoleLogic}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04OnRecordsSpatialConjunctionRoleLogic.pdf}
}

@TECHREPORT{ArkoudasETAL04VerifyingImplementationFileSystem,
  author = {Konstantine Arkoudas and Karen Zee and Viktor Kuncak and Martin Rinard},
  title = {On Verifying a File System Implementation},
  institution = {MIT CSAIL},
  year = 2004,
  number = 946,
  month = {May},
  note = {See also conference version 
          \cite{ArkoudasETAL04VerifyingFileSystemImplementationICFEM}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/ArkoudasETAL04VerifyingImplementationFileSystem.pdf}
}

@INPROCEEDINGS{KuncakRinard04BooleanAlgebraShapeAnalysisConstraints,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Boolean Algebra of Shape Analysis Constraints},
  booktitle = {Verification, Model Checking and Abstract Interpretation},
  series = {LNCS},
  volume = {2937},
  year = 2004,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard04BooleanAlgebraShapeAnalysisConstraints.pdf}
}

@TECHREPORT{KuncakLeino03OnComputingFixpoints,
  author = {Viktor Kuncak and K. Rustan M. Leino},
  title = {On computing the fixpoint of a set of boolean equations},
  institution = {Microsoft Research},
  year = 2003,
  number = {MSR-TR-2003-08},
  month = {December},
  url = {http://arxiv.org/abs/cs.PL/0408045},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakLeino03OnComputingFixpoints.pdf}
}

@TECHREPORT{LamETAL03OnModularPluggableAnalysesUsingSetInterfaces,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {On Modular Pluggable Analyses Using Set Interfaces},
  institution = {MIT CSAIL},
  month = {December},
  number = {933},
  year = 2003,
  localurl = {http://lara.epfl.ch/~kuncak/papers/LamETAL03OnModularPluggableAnalysesUsingSetInterfaces.pdf}
}

@ARTICLE{LamETAL04GeneralizedTypestateCheckingUsingSets,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses},
  journal = {SIGPLAN Notices},
  year = 2004,
  volume = 39,
  issue = 3,
  month = {March},
  pages = {46--55},
  localurl = {http://lara.epfl.ch/~kuncak/papers/LamETAL04GeneralizedTypestateCheckingUsingSets.pdf}
}

@TECHREPORT{KuncakRinard03OnRoleLogic,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On Role Logic},
  institution = {MIT CSAIL},
  number = 925,
  year = 2003,
  url = {http://arxiv.org/abs/cs.PL/0408018},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03OnRoleLogic.pdf}
}

@TECHREPORT{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On the Boolean Algebra of Shape Analysis Constraints},
  institution = {MIT CSAIL},
  year = 2003,
  month = {August},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints.pdf}
}

@INPROCEEDINGS{KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Structural Subtyping of Non-Recursive Types is Decidable},
  booktitle = {Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS)},
  publisher = {IEEE},
  isbn = {0-7695-1884-2},
  year = 2003,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable.pdf}
}

@INPROCEEDINGS{KuncakRinard03ExistentialHeapAbstractionEntailment,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Existential Heap Abstraction Entailment is Undecidable},
  booktitle = {10th Annual International Static Analysis Symposium},
  year = 2003,
  address = {San Diego, California},
  month = {June 11-13},
  series = {LNCS},
  volume = {2694},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03ExistentialHeapAbstractionEntailment.pdf}
}

@INPROCEEDINGS{KuncakLeino03InPlaceRefinementEffectChecking,
  author = {Viktor Kuncak and Rustan Leino},
  title = {In-Place Refinement for Effect Checking},
  booktitle = {Workshop on Automated Verification of 
                  Infinite-State Systems},
  year = 2003,
  month = {April},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakLeino03InPlaceRefinementEffectChecking.pdf}
}

@TECHREPORT{KuncakRinard03TheoryStructuralSubtyping,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On the Theory of Structural Subtyping},
  institution = {MIT LCS},
  number = 879,
  year = 2003,
  url = {http://arxiv.org/abs/cs.LO/0408015},
  note = {Technical report version of 
          \cite{KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable}},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.pdf}
}

@TECHREPORT{KuncakRinard02TypestateCheckingRegularGraphConstraints,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Typestate Checking and Regular Graph Constraints},
  institution = {MIT LCS},
  number = 863,
  year = 2002,
  url = {http://arxiv.org/abs/cs.PL/0408014},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard02TypestateCheckingRegularGraphConstraints.pdf}
}

@INPROCEEDINGS{KuncakETAL02RoleAnalysis,
  author = {Viktor Kuncak and Patrick Lam and Martin Rinard},
  title = {Role Analysis},
  booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
  ee = {http://doi.acm.org/10.1145/503272.503276},
  isbn = {1-58113-450-9},
  year = 2002,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL02RoleAnalysis.pdf}
}

@MASTERSTHESIS{Kuncak01DesigningRoleAnalysis,
  author = {Viktor Kuncak},
  title = {Designing an Algorithm for Role Analysis},
  school = {MIT LCS},
  year = 2001,
  localurl = {http://lara.epfl.ch/~kuncak/papers/Kuncak01DesigningRoleAnalysis.pdf}
}

@TECHREPORT{KuncakETAL01RolesTechRep,
  author = {Viktor Kuncak and Patrick Lam and Martin Rinard},
  title = {Roles are really great!},
  institution = {MIT LCS},
  number = 822,
  year = 2001,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL01RolesTechRep.pdf}
}

@INPROCEEDINGS{KuncakETAL01LanguageRoleSpecifications,
  author = {Viktor Kuncak and Patrick Lam and Martin Rinard},
  title = {A Language for Role Specifications},
  booktitle = {Workshop on Languages and Compilers for Parallel Computing},
  volume = 2624,
  series = {LNCS},
  year = 2001,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakETAL01LanguageRoleSpecifications.pdf}
}

@TECHREPORT{KuncakRinard01ObjectModelsHeapsInterpretations,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Object Models, Heaps, and Interpretations},
  institution = {MIT LCS},
  year = 2001,
  number = 816,
  month = {January},
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard01ObjectModelsHeapsInterpretations.pdf}
}

@ARTICLE{IvanovicKuncak02NumericalRepresentations,
  author = {Mirjana Ivanovi\'c and Viktor Kuncak},
  title = {Numerical Representations as Purely Functional Data Structures: A New Approach},
  journal = {INFORMATICA, Institute of Mathematics and Informatics, Vilnius},
  year = 2002,
  volume = 13,
  number = 2
}

@INPROCEEDINGS{GhilezanKuncak01TypesConfluence,
  author = {Silvia Ghilezan and Viktor Kuncak},
  title = {Types and confluence in lambda calculus},
  booktitle = {3rd Panhellenic Logic Symposium},
  pages = {17--21},
  year = 2001,
  address = {Anogia, Greece}
}

@INPROCEEDINGS{GhilezanKuncak01Confluence,
  author = {Silvia Ghilezan and Viktor Kuncak},
  title = {Confluence of untyped lambda calculus via simple types},
  booktitle = {Proceedings of the 7th Italian Conference on Theoretical Computer Science, ICTCS 2001},
  year = 2001,
  volume = 2202,
  series = {LNCS},
  address = {Torino, Italy},
  month = {October}
}

@INPROCEEDINGS{GhilezanETAL01Reducibility,
  author = {Silvia Ghilezan and Viktor Kuncak and Silvia Likavec},
  title = {Reducibility method for termination properties of typed lambda terms},
  booktitle = {Fifth International Workshop on Termination},
  year = 2001,
  address = {Utrecht, The Netherlands},
  month = {May}
}

@INPROCEEDINGS{IvanovicKuncak00ModularLanguageSpecificationsHaskell,
  author = {Mirjana Ivanovi\'c and Viktor Kuncak},
  title = {Modular Language Specifications in {H}askell},
  booktitle = {Theoretical Aspects of Computer Science 
                  with practical application},
  year = 2000,
  month = {September},
  localurl = {http://lara.epfl.ch/~kuncak/papers/IvanovicKuncak00ModularLanguageSpecificationsHaskell.pdf}
}

@MISC{Kuncak00ModularInterpretersHaskell,
  author = {Viktor Kuncak},
  title = {Modular Interpreters in {Haskell}},
  howpublished = {B.Sc. Thesis, University of Novi Sad},
  month = {8 June},
  year = 2000,
  note = {See \cite{IvanovicKuncak00ModularLanguageSpecificationsHaskell} 
                  for paper.},
  localurl = {http://lara.epfl.ch/~kuncak/papers/Kuncak00ModularInterpretersHaskell.pdf}
}

@INPROCEEDINGS{IvanovicKuncak01NumericalRepresentations,
  author = {Mirjana Ivanovi\'c and Viktor Kuncak},
  title = {Numerical Representations as Purely Functional Data Structures},
  booktitle = {XIV Conference on Applied Mathematics "PRIM", Pali\'c},
  year = 2000,
  month = {June},
  note = {Also in: Novi Sad J. Math. 31 (2001), no. 1, 141--149}
}

@INPROCEEDINGS{GhilezanKuncak01ReducibilityMethodPrim,
  author = {Silvia Ghilezan and Viktor Kuncak},
  title = {Reducibility Method in Simply Typed Lambda Calculus},
  booktitle = {XIV Conference on Applied Mathematics "PRIM", Pali\'c},
  year = 2000,
  month = {June},
  note = {Also in: Novi Sad J. Math. 31 (2001), no. 1, 27--32}
}

@MISC{VoigtlaenderKuncakMultigridSolver,
  author = {Janis Voigtl\"ander and Viktor Kuncak},
  title = {Developing a Multigrid Solver for Standing Wave Equation},
  howpublished = {Proceedings of the 28th Dr. Bessie F. Lawrence 
                  International Summer Science Institute Participants,
                  Weizmann Institute of Science},
  pages = {149--154},
  year = 1996,
  localurl = {http://lara.epfl.ch/~kuncak/papers/VoigtlaenderKuncakMultigridSolver.pdf}
}

@INPROCEEDINGS{Kuncak93PLS,
  author = {Viktor Kuncak},
  title = {{PLS}: Programming Language for Simulations},
  booktitle = {Proceedings of the Petnica Science Center Seminar '93},
  pages = {111--146},
  year = 1993,
  publisher = {Science Center Petnica, Valjevo, Yugoslavia},
  note = {in Serbian}
}