Viktor Kuncak

According to our database1, Viktor Kuncak authored at least 110 papers between 2001 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Minimal Synthesis of String to String Functions from Examples.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

2018
Bidirectional evaluation with direct manipulation.
PACMPL, 2018

2017
Towards a Compiler for Reals.
ACM Trans. Program. Lang. Syst., 2017

Solving quantified linear arithmetic by counterexample-guided instantiation.
Formal Methods in System Design, 2017

Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact).
DARTS, 2017

Contract-based resource verification for higher-order functions with memoization.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Proactive Synthesis of Recursive Tree-to-String Functions from Examples.
Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016
An Update on Deductive Synthesis and Repair in the Leon Tool.
Proceedings of the Proceedings Fifth Workshop on Synthesis, 2016

SMT-based checking of predicate-qualified types for Scala.
Proceedings of the 7th ACM SIGPLAN Symposium on Scala, 2016

Translating Scala Programs to Isabelle/HOL - System Description.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
On recursion-free Horn clauses and Craig interpolation.
Formal Methods in System Design, 2015

Induction for SMT Solvers.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

InSynth: A System for Code Completion using Types and Weights.
Proceedings of the Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März, 2015

Counter-example complete verification for higher-order functions.
Proceedings of the 6th ACM SIGPLAN Symposium on Scala, 2015

Sound reasoning about integral data types with a reusable SMT solver interface.
Proceedings of the 6th ACM SIGPLAN Symposium on Scala, 2015

Automating grammar comparison.
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Programming with enumerable sets of structures.
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Synthesizing Java expressions from free-form queries.
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Developing Verified Software Using Leon.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Interactive Synthesis Using Free-Form Queries.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Deductive Program Repair.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Checking Data Structure Properties Orders of Magnitude Faster.
Proceedings of the Runtime Verification - 5th International Conference, 2014

Sound compilation of reals.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution).
Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

SciFe: Scala framework for efficient enumeration of data structures with invariants.
Proceedings of the Fifth Annual Scala Workshop, 2014

Symbolic Resource Bound Inference for Functional Programs.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Functional synthesis for linear arithmetic and sets.
STTT, 2013

Software verification and graph similarity for automated evaluation of students' assignments.
Information & Software Technology, 2013

Classifying and Solving Horn Clauses for Verification.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Effect Analysis for Programs with Callbacks.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Reductions for Synthesis Procedures.
Proceedings of the Verification, 2013

Automatic synthesis of out-of-core algorithms.
Proceedings of the ACM SIGMOD International Conference on Management of Data, 2013

Executing Specifications Using Synthesis and Constraint Solving.
Proceedings of the Runtime Verification - 4th International Conference, 2013

Complete completion using types and weights.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Game programming by demonstration.
Proceedings of the ACM Symposium on New Ideas in Programming and Reflections on Software, 2013

Synthesis modulo recursive functions.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Interpolation for synthesis on unbounded domains.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Synthesis of fixed-point programs.
Proceedings of the International Conference on Embedded Software, 2013

An overview of the Leon verification system: verification by translation to recursive functions.
Proceedings of the 4th Workshop on Scala, 2013

Disjunctive Interpolants for Horn-Clause Verification.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012
Software synthesis procedures.
Commun. ACM, 2012

Abortable Linearizable Modules.
Archive of Formal Proofs, 2012

Deciding Functional Lists with Sublist Sets.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Certifying Solutions for Numerical Constraints.
Proceedings of the Runtime Verification, Third International Conference, 2012

Constraints as control.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Speculative linearizability.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

A Verification Toolkit for Numerical Transition Systems - Tool Paper.
Proceedings of the FM 2012: Formal Methods, 2012

Synthesis for Unbounded Bit-Vector Arithmetic.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Accelerating Interpolants.
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
Sets with Cardinality Constraints in Satisfiability Modulo Theories.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Towards Complete Reasoning about Axiomatic Specifications.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Satisfiability Modulo Recursive Programs.
Proceedings of the Static Analysis - 18th International Symposium, 2011

Trustworthy numerical computation in Scala.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Interactive Synthesis of Code Snippets.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

An Efficient Decision Procedure for Imperative Tree Data Structures.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Scala to the Power of Z3: Integrating SMT and Programming.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
Predicting and preventing inconsistencies in deployed distributed systems.
ACM Trans. Comput. Syst., 2010

Collections, Cardinalities, and Relations.
Proceedings of the Verification, 2010

Building a Calculus of Data Structures.
Proceedings of the Verification, 2010

Phantm: PHP analyzer for type mismatch.
Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis.
Proceedings of the Runtime Verification - First International Conference, 2010

Decision procedures for algebraic data types with abstractions.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Complete functional synthesis.
Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

Test generation through programming in UDITA.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Synthesis for regular specifications over unbounded domains.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Ordered Sets in the Calculus of Data Structures.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Comfusy: A Tool for Complete Functional Synthesis.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

MUNCH - Automated Reasoner for Sets and Multisets.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Opis: reliable distributed systems in OCaml.
Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

An integrated proof language for imperative programs.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems.
Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, 2009

Simplifying Distributed System Development.
Proceedings of HotOS'09: 12th Workshop on Hot Topics in Operating Systems, 2009

Combining Theories with Shared Set Operations.
Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

2008
Decision Procedures for Multisets with Cardinality Constraints.
Proceedings of the Verification, 2008

Runtime Checking for Separation Logic.
Proceedings of the Verification, 2008

Full functional verification of linked data structures.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Verifying linked data structure implementations.
Proceedings of the 22nd IEEE International Symposium on Parallel and Distributed Processing, 2008

Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Linear Arithmetic with Stars.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Modular data structure verification.
PhD thesis, 2007

Using First-Order Theorem Provers in the Jahob Data Structure Verification System.
Proceedings of the Verification, 2007

Runtime Checking for Program Verification.
Proceedings of the Runtime Verification, 7th International Workshop, 2007

Polynomial Constraints for Sets with Cardinality Bounds.
Proceedings of the Foundations of Software Science and Computational Structures, 2007

Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic.
Proceedings of the Automated Deduction, 2007

2006
Modular Pluggable Analyses for Data Structure Consistency.
IEEE Trans. Software Eng., 2006

Deciding Boolean Algebra with Presburger Arithmetic.
J. Autom. Reasoning, 2006

Field Constraint Analysis.
Proceedings of the Verification, 2006

An overview of the Jahob analysis system: project goals and current status.
Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

2005
Decision Procedures for Set-Valued Fields.
Electr. Notes Theor. Comput. Sci., 2005

Implications of a Data Structure Consistency Checking System.
Proceedings of the Verified Software: Theories, 2005

Generalized Typestate Checking for Data Structure Consistency.
Proceedings of the Verification, 2005

Relational analysis of algebraic datatypes.
Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

On Algorithms and Complexity for Sets with Cardinality Constraints.
Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

Hob: A Tool for Verifying Data Structure Consistency.
Proceedings of the Compiler Construction, 14th International Conference, 2005

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic.
Proceedings of the Automated Deduction, 2005

Crosscutting techniques in program specification and analysis.
Proceedings of the 4th International Conference on Aspect-Oriented Software Development, 2005

2004
Generalized typestate checking using set interfaces and pluggable analyses.
SIGPLAN Notices, 2004

File Refinement.
Archive of Formal Proofs, 2004

Binary Search Trees.
Archive of Formal Proofs, 2004

Boolean Algebra of Shape Analysis Constraints.
Proceedings of the Verification, 2004

Generalized Records and Spatial Conjunction in Role Logic.
Proceedings of the Static Analysis, 11th International Symposium, 2004

Verifying a File System Implementation.
Proceedings of the Formal Methods and Software Engineering, 2004

2003
Existential Heap Abstraction Entailment Is Undecidable.
Proceedings of the Static Analysis, 10th International Symposium, 2003

Structural Subtyping of Non-Recursive Types is Decidable.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

2002
Numerical Representations as Purely Functional Data Structures: a New Approach.
Informatica, Lith. Acad. Sci., 2002

Role analysis.
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

2001
A Language for Role Specifications.
Proceedings of the Languages and Compilers for Parallel Computing, 2001

Confluence of Untyped Lambda Calculus via Simple Types.
Proceedings of the Theoretical Computer Science, 7th Italian Conference, 2001


  Loading...