|
[178]
|
Simon Guilloud, Sankalp Ghambhir, and Viktor Kunčak.
Interpolation and quantifiers in ortholattices.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI). Springer International Publishing, 2024.
|
|
[177]
|
Simon Guilloud and Viktor Kunčak.
Orthologic with axioms.
Proc. ACM Program. Lang. (POPL), 8(POPL), jan 2024.
Keywords: Decision procedures, Logic and decidability, Verification, Orthologic
|
|
[176]
|
Dragana Milovančević and Viktor Kunčak.
Proving and disproving equivalence of functional programming
assignments.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2023.
|
|
[175]
|
Simon Guilloud, Mario Bucev, Dragana Milovančević, and Viktor
Kunčak.
Formula normalizations in verification.
In Computer-Aided Verification (CAV), 2023.
|
|
[174]
|
Simon Guilloud, Sankalp Ghambir, and Viktor Kunčak.
Lisa -- a proof assistant embedded in scala.
In Interactive Theorem Proving (ITP), 2023.
|
|
[173]
|
Rodrigo Raya, Jad Hamza, and Viktor Kuncak.
On the complexity of convex and reverse convex prequadratic
constraints.
In 24th Int. Conf. Logic for Programming, Artificial
Intelligence and Reasoning (LPAR), 2023.
|
|
[172]
|
Rodrigo Raya and Viktor Kunčak.
NP satisfiability for arrays as powers.
In Bernd Finkbeiner and Thomas Wies, editors, Verification,
Model Checking, and Abstract Interpretation (VMCAI), pages 301--318.
Springer International Publishing, 2022.
|
|
[171]
|
Georg Stefan Schmid and Viktor Kunčak.
Generalized arrays for Stainless frames.
In Bernd Finkbeiner and Thomas Wies, editors, Verification,
Model Checking, and Abstract Interpretation (VMCAI), pages 332--354.
Springer International Publishing, 2022.
|
|
[170]
|
Simon Guilloud and Viktor Kunčak.
Equivalence checking for orthocomplemented bisemilattices in
log-linear time.
In TACAS, 2022.
|
|
[169]
|
Jad Hamza, Simon Felix, Viktor Kunčak, Ivo Nussbaumer, and Filip Schramka.
From verified Scala to STIX file system embedded code using
Stainless.
In NASA Formal Methods (NFM), page 18, 2022.
|
|
[168]
|
Mario Bucev and Viktor Kunčak.
Formally verified Quite OK Image format.
In Formal Methods in Computer-Aided Design (FMCAD), 2022.
|
|
[167]
|
Viktor Kuncak and Jad Hamza.
Stainless verification system tutorial.
In Formal Methods in Computer Aided Design, FMCAD 2021, New
Haven, CT, USA, October 19-22, 2021, pages 2--7. IEEE, 2021.
|
|
[166]
|
Romain Edelmann, Jad Hamza, and Viktor Kunčak.
Zippy LL(1) parsing with derivatives.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2020.
|
|
[165]
|
Jad Hamza, Nicolas Voirol, and Viktor Kunčak.
System FR: Formalized foundations for the Stainless verifier.
Proc. ACM Program. Lang, (OOPSLA), November 2019.
|
|
[164]
|
Jad Hamza and Viktor Kunčak.
Minimal synthesis of string to string functions from examples.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), pages 48--69, 2019.
|
|
[163]
|
Mikaël Mayer, Viktor Kunčak, and Ravi Chugh.
Bidirectional evaluation with direct manipulation.
Proc. ACM Program. Lang, (OOPSLA, Article 127), November 2018.
|
|
[162]
|
Eva Darulova and Viktor Kuncak.
Towards a compiler for reals.
ACM Trans. Program. Lang. Syst. (TOPLAS), 39(2):8:1--8:28,
March 2017.
|
|
[161]
|
Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak.
Contract-based resource verification for higher-order functions with
memoization.
In ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages (POPL), 2017.
|
|
[160]
|
Mikaël Mayer, Jad Hamza, and Viktor Kuncak.
Proactive Synthesis of Recursive Tree-to-String Functions from
Examples.
In Peter Müller, editor, 31st European Conference on
Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz
International Proceedings in Informatics (LIPIcs), pages 19:1--19:30,
Dagstuhl, Germany, 2017. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
|
|
[159]
|
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, and Morgan
Deters.
Refutation-based synthesis in SMT.
Formal Methods in System Design (FMSD), 2017.
|
|
[158]
|
Andrew Reynolds, Tim King, and Viktor Kuncak.
Solving quantified linear arithmetic by counterexample-guided
instantiation.
Formal Methods in System Design (FMSD), 2017.
|
|
[157]
|
Lars Hupel and Viktor Kuncak.
Translating scala programs to isabelle/hol (system description).
In International Joint Conference on Automated Reasoning
(IJCAR), 2016.
|
|
[156]
|
Manos Koukoutos, Etienne Kneuss, and Viktor Kuncak.
An update on deductive synthesis and repair in the leon tool.
In 5th Workshop on Synthesis, 2016.
|
|
[155]
|
Georg Stefan Schmid and Viktor Kuncak.
SMT-based checking of predicate-qualified types for Scala.
In Scala Symposium, 2016.
|
|
[154]
|
Andrew Reynolds and Viktor Kuncak.
Induction for SMT solvers.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), 2015.
|
|
[153]
|
Viktor Kuncak.
Developing verified software using Leon (invited contribution).
In NASA Formal Methods (NFM), 2015.
|
|
[152]
|
Tihomir Gvero and Viktor Kuncak.
Interactive synthesis using free-form queries (tool demonstration).
In International Conference on Software Engineering (ICSE),
2015.
|
|
[151]
|
Régis Blanc and Viktor Kuncak.
Sound reasoning about integral data types with a reusable SMT
solver interface.
In Scala Symposium, 2015.
|
|
[150]
|
Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak.
Counter-example complete verification for higher-order functions.
In Scala Symposium, 2015.
|
|
[149]
|
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark
Barrett.
Counterexample guided quantifier instantiation for synthesis in
SMT.
In Computer-Aided Verification (CAV), 2015.
|
|
[148]
|
Etienne Kneuss, Manos Koukoutos, and Viktor Kuncak.
Deductive program repair.
In Computer-Aided Verification (CAV), 2015.
|
|
[147]
|
Ravichandhran Madhavan, Mikael Mayer, Sumit Gulwani, and Viktor Kuncak.
Automating grammar comparison.
In OOPSLA, 2015.
|
|
[146]
|
Tihomir Gvero and Viktor Kuncak.
Synthesizing java expressions from free-form queries.
In OOPSLA, 2015.
|
|
[145]
|
Ivan Kuraj, Viktor Kuncak, and Daniel Jackson.
Programming with enumerable sets of structures.
In OOPSLA, 2015.
|
|
[144]
|
Eva Darulova and Viktor Kuncak.
Sound compilation of reals.
In ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages (POPL), 2014.
|
|
[143]
|
Ravichandhran Madhavan and Viktor Kuncak.
Symbolic resource bound inference for functional programs.
In Computer Aided Verification (CAV), 2014.
|
|
[142]
|
Viktor Kuncak.
Verifying and synthesizing software with recursive functions (invited
contribution).
In 41st International Colloquium on Automata, Languages, and
Programming (ICALP), 2014.
|
|
[141]
|
Emmanouil Koukoutos and Viktor Kuncak.
Checking data structure properties orders of magnitude faster.
In Runtime Verification (RV), 2014.
|
|
[140]
|
Ivan Kuraj and Viktor Kuncak.
Scife: Scala framework for efficient enumeration of data structures
with invariants.
In Scala Workshop, 2014.
|
|
[139]
|
Viktor Kuncak, Etienne Kneuss, and Emmanouil Koukoutos.
Synthesizing functions from relations in Leon (invited
contribution).
In Logic-Based Program Synthesis and Transformation (LOPSTR),
2014.
|
|
[138]
|
Tihomir Gvero and Viktor Kuncak.
On synthesizing code from free-form queries.
Technical Report EPFL-REPORT-201606, EPFL, 2014.
|
|
[137]
|
Andrew Reynolds and Viktor Kuncak.
On induction for SMT solvers.
Technical Report EPFL-REPORT-201755, EPFL, 2014.
|
|
[136]
|
Ravichandhran Madhavan and Viktor Kuncak.
On template-based inference of rich invariants in Leon.
Technical Report EPFL-REPORT-190578, EPFL, November 2013.
|
|
[135]
|
Swen Jacobs, Viktor Kuncak, and Phillippe Suter.
Reductions for synthesis procedures.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), 2013.
|
|
[134]
|
Milena Vujošević-Janičić, Mladen Nikolić, Dušan
Tošić, and Viktor Kuncak.
Software verification and graph similarity for automated evaluation
of students' assignments.
Information and Software Technology, 2013.
|
|
[133]
|
Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac.
Complete completion using types and weights.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2013.
|
|
[132]
|
Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak.
Disjunctive interpolants for horn-clause verification.
In Computer Aided Verification (CAV), 2013.
|
|
[131]
|
Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, and Philippe Suter.
On integrating deductive synthesis and verification systems.
Technical Report EPFL-REPORT-186043, EPFL, 2013.
|
|
[130]
|
Régis William Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter.
On verification by translation to recursive functions.
Technical Report EPFL-REPORT-186233, EPFL, 2013.
|
|
[129]
|
Andrej Spielmann, Andres Nötzli, Christoph Koch, Viktor Kuncak, and Yannis
Klonatos.
Automatic synthesis of out-of-core algorithms.
In SIGMOD, 2013.
|
|
[128]
|
Régis William Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter.
An overview of the Leon verification system: Verification by
translation to recursive functions.
In Scala Workshop, 2013.
|
|
[127]
|
Viktor Kuncak, Etienne Kneuss, and Philippe Suter.
Executing specifications using synthesis and constraint solving
(invited talk).
In Runtime Verification (RV), 2013.
|
|
[126]
|
Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak.
Classifying and solving horn clauses for verification.
In Fifth Working Conference on Verified Software: Theories,
Tools and Experiments, 2013.
|
|
[125]
|
Etienne Kneuss, Viktor Kuncak, and Philippe Suter.
Effect analysis for programs with callbacks.
In Fifth Working Conference on Verified Software: Theories,
Tools and Experiments, 2013.
|
|
[124]
|
Eva Darulova, Viktor Kuncak, Rupak Majumdar, and Indranil Saha.
Synthesis of fixed-point programs.
In Embedded Software (EMSOFT), 2013.
|
|
[123]
|
Viktor Kuncak and Régis Blanc.
Interpolation for synthesis on unbounded domains.
In Formal Methods in Computer-Aided Design (FMCAD), 2013.
|
|
[122]
|
Mikaël Mayer and Viktor Kuncak.
Game programming by demonstration.
In SPLASH Onward!, 2013.
|
|
[121]
|
Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, and Philippe Suter.
Synthesis modulo recursive functions.
In OOPSLA, 2013.
|
|
[120]
|
Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter.
Constraints as control.
In ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages (POPL), 2012.
|
|
[119]
|
Milena Vujošević-Janičić and Viktor Kuncak.
Development and evaluation of LAV: an SMT-based error finding
platform.
In Verified Software: Theories, Tools and Experiments (VSTTE),
LNCS, 2012.
|
|
[118]
|
Thomas Wies, Marco Mu niz, and Viktor Kuncak.
Deciding functional lists with sublist sets.
In Verified Software: Theories, Tools and Experiments (VSTTE),
LNCS, 2012.
|
|
[117]
|
Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter.
Functional synthesis for linear arithmetic and sets.
Software Tools for Technology Transfer (STTT), TBD(TBD), 2012.
|
|
[116]
|
Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter.
Software synthesis procedures.
Communications of the ACM, 2012.
|
|
[115]
|
Rachid Guerraoui, Viktor Kuncak, and Giuliano Losa.
Speculative linearizability.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2012.
|
|
[114]
|
Andrej Spielmann and Viktor Kuncak.
Synthesis for unbounded bitvector arithmetic.
In International Joint Conference on Automated Reasoning
(IJCAR), LNAI. Springer, 2012.
|
|
[113]
|
Hossein Hojjat, Filip Konecny, Florent Garnier, Radu Iosif, Viktor Kuncak, and
Philipp Ruemmer.
A verification toolkit for numerical transition systems (tool paper).
In 16th International Symposium on Formal Methods (FM).
Springer, 2012.
|
|
[112]
|
Hossein Hojjat, Radu Iosif, Filip Konečný, Viktor Kuncak, and Philipp
Rümmer.
Accelerating interpolants.
In Automated Technology for Verification and Analysis (ATVA),
2012.
|
|
[111]
|
Eva Darulova and Viktor Kuncak.
Certifying solutions for numerical constraints.
In Runtime Verification (RV), 2012.
|
|
[110]
|
Swen Jacobs and Viktor Kuncak.
Towards complete reasoning about axiomatic specifications.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), 2011.
|
|
[109]
|
Philippe Suter, Robin Steiger, and Viktor Kuncak.
Sets with cardinality constraints in satisfiability modulo theories.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), 2011.
|
|
[108]
|
Tihomir Gvero, Viktor Kuncak, and Ruzica Piskac.
Interactive synthesis of code snippets.
In Computer Aided Verification (CAV) Tool Demo, 2011.
|
|
[107]
|
Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter.
Scala to the power of Z3: Integrating SMT and programming.
In Computer-Aideded Deduction (CADE) Tool Demo, 2011.
|
|
[106]
|
Thomas Wies, Marco Muñiz, and Viktor Kuncak.
An efficient decision procedure for imperative tree data structures.
In Computer-Aideded Deduction (CADE), 2011.
|
|
[105]
|
Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak.
Satisfiability modulo recursive programs.
In Static Analysis Symposium (SAS), 2011.
|
|
[104]
|
Eva Darulová and Viktor Kuncak.
Trustworthy numerical computation in scala.
In OOPSLA, 2011.
|
|
[103]
|
Swen Jacobs and Viktor Kuncak.
On locality of one-variable axioms and piecewise combinations.
Technical Report EPFL-REPORT-148180, EPFL, April 2010.
|
|
[102]
|
Thomas Wies, Marco Mu niz, and Viktor Kuncak.
On deciding functional lists with sublist sets.
Technical Report EPFL-REPORT-148361, EPFL, April 2010.
|
|
[101]
|
Philippe Suter, Mirco Dotta, and Viktor Kuncak.
Decision procedures for algebraic data types with abstractions.
In ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages (POPL), 2010.
|
|
[100]
|
Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak.
Collections, cardinalities, and relations.
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), 2010.
|
|
[99]
|
Viktor Kuncak, Ruzica Piskac, Philippe Suter, and Thomas Wies.
Building a calculus of data structures (invited paper).
In Verification, Model Checking, and Abstract Interpretation
(VMCAI), 2010.
|
|
[98]
|
Maysam Yabandeh, Nikola Knežević, Dejan Kostić, and Viktor Kuncak.
Predicting and preventing inconsistencies in deployed distributed
systems.
ACM Transactions on Computer Systems, 28(1), 2010.
|
|
[97]
|
Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor
Kuncak, and Darko Marinov.
Test generation through programming in UDITA.
In International Conference on Software Engineering (ICSE),
2010.
|
|
[96]
|
Ruzica Piskac, Philippe Suter, and Viktor Kuncak.
On decision procedures for ordered collections.
Technical Report LARA-REPORT-2010-001, EPFL, 2010.
|
|
[95]
|
Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter.
Complete functional synthesis.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2010.
|
|
[94]
|
Viktor Kuncak, Mikael Mayer, Ruzica Piskac, and Philippe Suter.
Comfusy: Complete functional synthesis (tool presentation).
In CAV, 2010.
|
|
[93]
|
Ruzica Piskac and Viktor Kuncak.
Munch - automated reasoner for sets and multisets (system
description).
In IJCAR, 2010.
|
|
[92]
|
Viktor Kuncak, Ruzica Piskac, and Philippe Suter.
Ordered sets in the calculus of data structures (invited paper).
In CSL, 2010.
|
|
[91]
|
Jad Hamza, Barbara Jobstmann, and Viktor Kuncak.
Synthesis for regular specifications over unbounded domains.
In FMCAD, 2010.
|
|
[90]
|
Etienne Kneuss, Philippe Suter, and Viktor Kuncak.
Runtime instrumentation for precise flow-sensitive type analysis.
In International Conference on Runtime Verification, 2010.
|
|
[89]
|
Etienne Kneuss, Philippe Suter, and Viktor Kuncak.
Phantm: PHP analyzer for type mismatch (research demonstration).
In ACM SIGSOFT Conference on Foundations of Software Engineering
(FSE), 2010.
|
|
[88]
|
Eva Darulova and Viktor Kuncak.
On rigorous numerical computation as a scala library.
Technical Report EPFL-REPORT-158754, EPFL, 2010.
|
|
[87]
|
Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak.
On satisfiability modulo computable functions.
Technical Report EPFL-REPORT, EPFL, 2010.
|
|
[86]
|
Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor
Kuncak, and Darko Marinov.
On test generation through programming in UDITA.
Technical Report LARA-REPORT-2009-05, EPFL, IC, September 2009.
|
|
[85]
|
Kuat Yessenov, Viktor Kuncak, and Ruzica Piskac.
On decision procedures for collections, cardinalities, and relations.
Technical Report LARA-REPORT-2009-004, EPFL, August 2009.
|
|
[84]
|
Philippe Suter, Mirco Dotta, and Viktor Kuncak.
On decision procedures for algebraic data types with abstractions.
Technical Report LARA-REPORT-2009-003, EPFL, July 2009.
|
|
[83]
|
Thomas Wies, Ruzica Piskac, and Viktor Kuncak.
On combining theories with shared set operations.
Technical Report LARA-REPORT-2009-002, EPFL, May 2009.
|
|
[82]
|
Viktor Kuncak and Thomas Wies.
On set-driven combination of logics and verifiers.
Technical Report LARA-REPORT-2009-001, EPFL, February 2009.
|
|
[81]
|
Pierre-Évariste Dagand, Dejan Kostić, and Viktor Kuncak.
Opis: Reliable distributed systems in OCaml.
In ACM SIGPLAN TLDI, 2009.
|
|
[80]
|
Maysam Yabandeh, Nikola Knežević, Dejan Kostić, and Viktor Kuncak.
CrystalBall: Predicting and preventing inconsistencies in deployed
distributed systems.
In 6th USENIX Symp. Networked Systems Design and Implementation
(NSDI '09), 2009.
|
|
[79]
|
Maysam Yabandeh, Nedeljko Vasić, Dejan Kostić, and Viktor Kuncak.
Simplifying distributed system development.
Technical Report NSL-REPORT-2009-001, EPFL, 2009.
|
|
[78]
|
Karen Zee, Viktor Kuncak, and Martin Rinard.
An integrated proof language for imperative programs.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2009.
|
|
[77]
|
Maysam Yabandeh, Nedeljko Vasić, Dejan Kostić, and Viktor Kuncak.
Simplifying distributed system development.
In 12th Workshop on Hot Topics in Operating Systems, 2009.
|
|
[76]
|
Thomas Wies, Ruzica Piskac, and Viktor Kuncak.
Combining theories with shared set operations.
In FroCoS: Frontiers in Combining Systems, 2009.
|
|
[75]
|
Philippe Suter, Ruzica Piskac, Mikael Mayer, and Viktor Kuncak.
On complete functional synthesis.
Technical Report LARA-REPORT-2009-006, EPFL, 2009.
|
|
[74]
|
Viktor Kuncak.
Constraint solving for software reliability and text analysis
(research plan).
Technical Report LARA-REPORT-2008-007, EPFL, August 2008.
|
|
[73]
|
Maysam Yabandeh, Nikola Knežević, Dejan Kostić, and Viktor Kuncak.
CrystalBall: Predicting and preventing inconsistencies in deployed
distributed systems.
Technical Report LARA-REPORT-2008-006, EPFL-IC-LARA, May 2008.
|
|
[72]
|
Huu Hai Nguyen, Viktor Kuncak, and Wei Ngan Chin.
Runtime checking for separation logic.
In 9th International Conference on Verification, Model Checking,
and Abstract Interpretation (VMCAI), LNCS, 2008.
|
|
[71]
|
Ruzica Piskac and Viktor Kuncak.
Decision procedures for multisets with cardinality constraints.
In 9th International Conference on Verification, Model Checking,
and Abstract Interpretation (VMCAI), LNCS, 2008.
|
|
[70]
|
Mirco Dotta, Philippe Suter, and Viktor Kuncak.
On static analysis for expressive pattern matching.
Technical Report LARA-REPORT-2008-004, EPFL, 2008.
|
|
[69]
|
Ruzica Piskac and Viktor Kuncak.
On linear arithmetic with stars.
Technical Report LARA-REPORT-2008-005, EPFL, 2008.
|
|
[68]
|
Karen Zee, Viktor Kuncak, and Martin Rinard.
Full functional verification of linked data structures.
In ACM SIGPLAN Conf. Programming Language Design and
Implementation (PLDI), 2008.
see also
[61].
|
|
[67]
|
Ruzica Piskac and Viktor Kuncak.
Linear arithmetic with stars.
In Computed-Aided Verification (CAV), volume 5123 of
LNCS, 2008.
|
|
[66]
|
Ruzica Piskac and Viktor Kuncak.
Fractional collections with cardinality bounds, and mixed integer
linear arithmetic with stars.
In Computer Science Logic (CSL), 2008.
|
|
[65]
|
Pierre-Évariste Dagand, Dejan Kostić, and Viktor Kuncak.
Opis: Reliable distributed systems in OCaml.
Technical Report NSL-REPORT-2008-001, EPFL-IC-NSL, 2008.
|
|
[64]
|
Milos Gligoric, Tihomir Gvero, Sarfraz Khurshid, Viktor Kuncak, and Darko
Marinov.
On delayed choice execution for falsification.
Technical Report LARA-REPORT-2008-08, EPFL, IC, 2008.
|
|
[63]
|
Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard.
Using first-order theorem provers in the Jahob data structure
verification system.
In Verification, Model Checking and Abstract Interpretation,
volume 4349 of LNCS, November 2007.
See [53] for full
version.
|
|
[62]
|
Bruno Marnette, Viktor Kuncak, and Martin Rinard.
Polynomial constraints for sets with cardinality bounds.
In Foundations of Software Science and Computation Structures
(FOSSACS), volume 4423 of LNCS, March 2007.
|
|
[61]
|
Viktor Kuncak.
Modular Data Structure Verification.
PhD thesis, EECS Department, Massachusetts Institute of Technology,
February 2007.
|
|
[60]
|
Viktor Kuncak.
Quantifier-free boolean algebra with presburger arithmetic is
np-complete.
Technical Report MIT-CSAIL-TR-2007-001, MIT CSAIL, January 2007.
|
|
[59]
|
Karen Zee, Viktor Kuncak, Michael Taylor, and Martin Rinard.
Runtime checking for program verification.
In Workshop on Runtime Verification, volume 4839 of LNCS,
2007.
|
|
[58]
|
Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard.
Verifying complex properties using symbolic shape analysis.
In Workshop on Heap Abstraction and Verification (collocated
with ETAPS), 2007.
|
|
[57]
|
Viktor Kuncak and Martin Rinard.
Towards efficient satisfiability checking for Boolean Algebra
with Presburger Arithmetic.
In Conference on Automateded Deduction (CADE-21), volume 4603
of LNCS, 2007.
|
|
[56]
|
Huu Hai Nguyen, Viktor Kuncak, and Wei Ngan Chin.
Runtime checking for separation logic.
Technical Report LARA-REPORT-2007-003, EPFL, 2007.
|
|
[55]
|
Ruzica Piskac and Viktor Kuncak.
Decision procedures for multisets with cardinality constraints.
Technical Report LARA-REPORT-2007-002, EPFL, 2007.
|
|
[54]
|
Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard.
Modular pluggable analyses for data structure consistency.
IEEE Transactions on Software Engineering (TSE), 32(12),
December 2006.
|
|
[53]
|
Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard.
On using first-order theorem provers in a the Jahob data structure
verification system.
Technical Report MIT-CSAIL-TR-2006-072, MIT, November 2006.
Full version of
[63].
|
|
[52]
|
Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard.
Field constraint analysis.
In Proc. Int. Conf. Verification, Model Checking, and Abstract
Interpratation, volume 3855 of LNCS, 2006.
See [48] for full version.
|
|
[51]
|
Viktor Kuncak and Martin Rinard.
An overview of the Jahob analysis system: Project goals and current
status.
In NSF Next Generation Software Workshop, 2006.
|
|
[50]
|
Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard.
Deciding Boolean Algebra with Presburger Arithmetic.
Journal of Automated Reasoning, 36(3), 2006.
|
|
[49]
|
Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard.
On verifying complex properties using symbolic shape analysis.
Technical Report MPI-I-2006-2-1, Max-Planck Institute for Computer
Science, 2006.
|
|
[48]
|
Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard.
On field constraint analysis.
Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010, MIT CSAIL,
November 2005.
Full version of [52].
|
|
[47]
|
Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard.
Implications of a data structure consistency checking system.
In International conference on Verified Software: Theories,
Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference), Zürich,
Switzerland, October 2005.
|
|
[46]
|
Bruno Marnette, Viktor Kuncak, and Martin Rinard.
On algorithms and complexity for sets with cardinality constraints.
Technical report, MIT CSAIL, August 2005.
|
|
[45]
|
Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard.
An algorithm for deciding BAPA: Boolean Algebra with
Presburger Arithmetic.
In 20th International Conference on Automated Deduction,
CADE-20, volume 3632 of LNCS, Tallinn, Estonia, July 2005.
Superseded by
[50].
|
|
[44]
|
Patrick Lam, Viktor Kuncak, and Martin Rinard.
Hob: A tool for verifying data structure consistency.
In 14th International Conference on Compiler Construction (tool
demo), volume 3443 of LNCS, April 2005.
|
|
[43]
|
Viktor Kuncak and Daniel Jackson.
On relational analysis of algebraic datatypes.
Technical Report 985, MIT, April 2005.
Full version of
[39].
|
|
[42]
|
Patrick Lam, Viktor Kuncak, and Martin Rinard.
Cross-cutting techniques in program specification and analysis.
In 4th International Conference on Aspect-Oriented Software
Development. ACM, March 2005.
|
|
[41]
|
Patrick Lam, Viktor Kuncak, and Martin Rinard.
Generalized typestate checking for data structure consistency.
In Verification, Model Checking and Abstract Interpretation,
volume 3385 of LNCS, 2005.
|
|
[40]
|
Viktor Kuncak and Martin C. Rinard.
Decision procedures for set-valued fields.
Electr. Notes Theor. Comput. Sci.; Proc. Abstract Interpretation
of Object-Oriented Languages, 131:51--62, 2005.
See [36] for full
version.
|
|
[39]
|
Viktor Kuncak and Daniel Jackson.
Relational analysis of algebraic datatypes.
In 10th European Soft. Eng. Conf. (ESEC) and 13th Symp.
Foundations of Software Engineering (FSE), 2005.
See [43] for
full version.
|
|
[38]
|
Karen Zee and Viktor Kuncak.
File refinement.
The Archive of Formal Proofs, December 2004.
Formal proof development.
|
|
[37]
|
Karen Zee, Patrick Lam, Viktor Kuncak, and Martin Rinard.
Combining theorem proving with static analysis for data structure
consistency.
In International Workshop on Software Verification and
Validation, Seattle, November 2004.
|
|
[36]
|
Viktor Kuncak and Martin Rinard.
On decision procedures for set-valued fields.
Technical Report 975, MIT CSAIL, November 2004.
Full version of
[40].
|
|
[35]
|
Viktor Kuncak and Martin Rinard.
On spatial conjunction as second-order logic.
Technical Report 970, MIT CSAIL, October 2004.
|
|
[34]
|
Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard.
Modular pluggable analyses for data structure consistency.
In Monterey Workshop on Software Engineering Tools:
Compatibility and Integration, Vienna, Austria, October 2004.
Superseded by
[?].
|
|
[33]
|
Patrick Lam, Viktor Kuncak, and Martin Rinard.
On our experience with modular pluggable analyses.
Technical Report 965, MIT CSAIL, September 2004.
|
|
[32]
|
Viktor Kuncak and Martin Rinard.
Generalized records and spatial conjunction in role logic.
In International Static Analysis Symposium, volume 3148 of
LNCS, Verona, Italy, August 2004.
See [29] for
full version.
|
|
[31]
|
Viktor Kuncak and Martin Rinard.
The first-order theory of sets with cardinality constraints is
decidable.
Technical Report 958, MIT CSAIL, July 2004.
Superseded by
[50].
|
|
[30]
|
Konstantine Arkoudas, Karen Zee, Viktor Kuncak, and Martin Rinard.
On verifying a file system implementation.
Technical Report 946, MIT CSAIL, May 2004.
See also conference version
[25].
|
|
[29]
|
Viktor Kuncak and Martin Rinard.
On generalized records and spatial conjunction in role logic.
Technical Report 942, MIT CSAIL, April 2004.
Full version of [32].
|
|
[28]
|
Viktor Kuncak.
Binary search trees.
The Archive of Formal Proofs, April 2004.
Formal proof development.
|
|
[27]
|
Patrick Lam, Viktor Kuncak, and Martin Rinard.
Generalized typestate checking using set interfaces and pluggable
analyses.
SIGPLAN Notices, 39:46--55, March 2004.
|
|
[26]
|
Viktor Kuncak and Martin Rinard.
Boolean algebra of shape analysis constraints.
In Verification, Model Checking and Abstract Interpretation,
volume 2937 of LNCS, 2004.
|
|
[25]
|
Konstantine Arkoudas, Karen Zee, Viktor Kuncak, and Martin Rinard.
Verifying a file system implementation.
In Sixth International Conference on Formal Engineering
Methods, volume 3308 of LNCS, Seattle, 2004.
See also technical report
[25].
|
|
[24]
|
Patrick Lam, Viktor Kuncak, and Martin Rinard.
On modular pluggable analyses using set interfaces.
Technical Report 933, MIT CSAIL, December 2003.
|
|
[23]
|
Viktor Kuncak and K. Rustan M. Leino.
On computing the fixpoint of a set of boolean equations.
Technical Report MSR-TR-2003-08, Microsoft Research, December 2003.
|
|
[22]
|
Viktor Kuncak and Martin Rinard.
On the boolean algebra of shape analysis constraints.
Technical report, MIT CSAIL, August 2003.
|
|
[21]
|
Viktor Kuncak and Martin Rinard.
Existential heap abstraction entailment is undecidable.
In 10th Annual International Static Analysis Symposium, volume
2694 of LNCS, San Diego, California, June 2003.
|
|
[20]
|
Viktor Kuncak and Rustan Leino.
In-place refinement for effect checking.
In Workshop on Automated Verification of Infinite-State
Systems, April 2003.
|
|
[19]
|
Viktor Kuncak and Martin Rinard.
On the theory of structural subtyping.
Technical Report 879, MIT LCS, 2003.
Technical report version of
[18].
|
|
[18]
|
Viktor Kuncak and Martin Rinard.
Structural subtyping of non-recursive types is decidable.
In Eighteenth Annual IEEE Symposium on Logic in Computer Science
(LICS). IEEE, 2003.
|
|
[17]
|
Viktor Kuncak and Martin Rinard.
On role logic.
Technical Report 925, MIT CSAIL, 2003.
|
|
[16]
|
Mirjana Ivanović and Viktor Kuncak.
Numerical representations as purely functional data structures: A new
approach.
INFORMATICA, Institute of Mathematics and Informatics, Vilnius,
13(2), 2002.
|
|
[15]
|
Viktor Kuncak, Patrick Lam, and Martin Rinard.
Role analysis.
In ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages (POPL), 2002.
|
|
[14]
|
Viktor Kuncak and Martin Rinard.
Typestate checking and regular graph constraints.
Technical Report 863, MIT LCS, 2002.
|
|
[13]
|
Silvia Ghilezan and Viktor Kuncak.
Confluence of untyped lambda calculus via simple types.
In Proceedings of the 7th Italian Conference on Theoretical
Computer Science, ICTCS 2001, volume 2202 of LNCS, Torino, Italy,
October 2001.
|
|
[12]
|
Silvia Ghilezan, Viktor Kuncak, and Silvia Likavec.
Reducibility method for termination properties of typed lambda terms.
In Fifth International Workshop on Termination, Utrecht, The
Netherlands, May 2001.
|
|
[11]
|
Silvia Ghilezan and Viktor Kuncak.
Types and confluence in lambda calculus.
In 3rd Panhellenic Logic Symposium, pages 17--21, Anogia,
Greece, 2001.
|
|
[10]
|
Viktor Kuncak and Martin Rinard.
Object models, heaps, and interpretations.
Technical Report 816, MIT LCS, January 2001.
|
|
[9]
|
Viktor Kuncak, Patrick Lam, and Martin Rinard.
A language for role specifications.
In Workshop on Languages and Compilers for Parallel Computing,
volume 2624 of LNCS, 2001.
|
|
[8]
|
Viktor Kuncak, Patrick Lam, and Martin Rinard.
Roles are really great!
Technical Report 822, MIT LCS, 2001.
|
|
[7]
|
Viktor Kuncak.
Designing an algorithm for role analysis.
Master's thesis, MIT LCS, 2001.
|
|
[6]
|
Mirjana Ivanović and Viktor Kuncak.
Modular language specifications in Haskell.
In Theoretical Aspects of Computer Science with practical
application, September 2000.
|
|
[5]
|
Silvia Ghilezan and Viktor Kuncak.
Reducibility method in simply typed lambda calculus.
In XIV Conference on Applied Mathematics "PRIM", Palić, June
2000.
Also in: Novi Sad J. Math. 31 (2001), no. 1, 27--32.
|
|
[4]
|
Mirjana Ivanović and Viktor Kuncak.
Numerical representations as purely functional data structures.
In XIV Conference on Applied Mathematics "PRIM", Palić, June
2000.
Also in: Novi Sad J. Math. 31 (2001), no. 1, 141--149.
|
|
[3]
|
Viktor Kuncak.
Modular interpreters in Haskell.
B.Sc. Thesis, University of Novi Sad, June 2000.
See [6] for
paper.
|
|
[2]
|
Janis Voigtländer and Viktor Kuncak.
Developing a multigrid solver for standing wave equation.
Proceedings of the 28th Dr. Bessie F. Lawrence International Summer
Science Institute Participants, Weizmann Institute of Science, 1996.
|
|
[1]
|
Viktor Kuncak.
PLS: Programming language for simulations.
In Proceedings of the Petnica Science Center Seminar '93, pages
111--146. Science Center Petnica, Valjevo, Yugoslavia, 1993.
in Serbian.
|