The following pages link to Viktor Kuncak (Q746766):
Displaying 48 items.
- On recursion-free Horn clauses and Craig interpolation (Q746767) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- Solving quantified linear arithmetic by counterexample-guided instantiation (Q1688537) (← links)
- Counterexample-guided quantifier instantiation for synthesis in SMT (Q1702893) (← links)
- (Q2152658) (redirect page) (← links)
- NP satisfiability for arrays as powers (Q2152659) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- Refutation-based synthesis in SMT (Q2280222) (← links)
- Minimal synthesis of string to string functions from examples (Q2287070) (← links)
- Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
- Synthesis for Unbounded Bit-Vector Arithmetic (Q2908521) (← links)
- Reductions for Synthesis Procedures (Q2926641) (← links)
- Towards Complete Reasoning about Axiomatic Specifications (Q3075488) (← links)
- Sets with Cardinality Constraints in Satisfiability Modulo Theories (Q3075499) (← links)
- (Q3148997) (← links)
- Linear Arithmetic with Stars (Q3512499) (← links)
- Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars (Q3540175) (← links)
- Ordered Sets in the Calculus of Data Structures (Q3586032) (← links)
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic (Q3608775) (← links)
- Combining Theories with Shared Set Operations (Q3655212) (← links)
- Building a Calculus of Data Structures (Q3656874) (← links)
- Collections, Cardinalities, and Relations (Q3656897) (← links)
- (Q4424843) (← links)
- (Q4448356) (← links)
- Accelerating Interpolants (Q4649296) (← links)
- (Q4794072) (← links)
- (Q4813414) (← links)
- (Q4922308) (← links)
- (Q4924969) (← links)
- Verifying and Synthesizing Software with Recursive Functions (Q5167727) (← links)
- Induction for SMT Solvers (Q5172636) (← links)
- Role analysis (Q5178895) (← links)
- Scala to the Power of Z3: Integrating SMT and Programming (Q5200039) (← links)
- An Efficient Decision Procedure for Imperative Tree Data Structures (Q5200043) (← links)
- Decision procedures for algebraic data types with abstractions (Q5255074) (← links)
- Contract-based resource verification for higher-order functions with memoization (Q5370871) (← links)
- Automated Deduction – CADE-20 (Q5394619) (← links)
- Sound compilation of reals (Q5408419) (← links)
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System (Q5452598) (← links)
- Runtime Checking for Separation Logic (Q5452718) (← links)
- Decision Procedures for Multisets with Cardinality Constraints (Q5452719) (← links)
- Static Analysis (Q5466572) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5711506) (← links)
- MUNCH - Automated Reasoner for Sets and Multisets (Q5747757) (← links)
- Polynomial Constraints for Sets with Cardinality Bounds (Q5758056) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5898616) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5901903) (← links)
- On algebraic array theories (Q6192058) (← links)
