StarExec

swMATH8839MaRDI QIDQ20838

No author found.

Related Items (62)

A decision procedure for (co)datatypes in SMT solvers ⋮ A Calculus for Modular Loop Acceleration ⋮ The 2013 evaluation of SMT-COMP and SMT-LIB ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ A Polymorphic Vampire ⋮ Confluence Competition 2015 ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ SAT race 2015 ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Machine learning-based restart policy for CDCL SAT solvers ⋮ Splitting proofs for interpolation ⋮ Scavenger 0.1: a theorem prover based on conflict resolution ⋮ Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems ⋮ Symmetry avoidance in MACE-style finite model finding ⋮ An empirical study of branching heuristics through the lens of global learning rate ⋮ Incremental bounded model checking for embedded software ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Deciding local theory extensions via E-matching ⋮ Counterexample-guided quantifier instantiation for synthesis in SMT ⋮ Unnamed Item ⋮ Induction with generalization in superposition reasoning ⋮ Unnamed Item ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ Proving Termination Through Conditional Termination ⋮ Scaling Enumerative Program Synthesis via Divide and Conquer ⋮ An efficient SMT solver for string constraints ⋮ Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19--22, 2014. Proceedings ⋮ Refutation-based synthesis in SMT ⋮ Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem ⋮ Superposition for \(\lambda\)-free higher-order logic ⋮ A FOOLish encoding of the next state relations of imperative programs ⋮ Datatypes with shared selectors ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers ⋮ Selecting the Selection ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Learning Rate Based Branching Heuristic for SAT Solvers ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers ⋮ Finding Finite Models in Multi-sorted First-Order Logic ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Restricted combinatory unification ⋮ Old or heavy? Decaying gracefully with age/weight shapes ⋮ Induction in saturation-based proof search ⋮ Faster, higher, stronger: E 2.3 ⋮ SAT competition 2020 ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Subsumption demodulation in first-order theorem proving ⋮ Layered clause selection for theory reasoning (short paper) ⋮ Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description) ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10 ⋮ The SDEval benchmarking toolkit ⋮ Learning Optimal Decision Sets and Lists with SAT ⋮ SAT-Inspired Eliminations for Superposition

This page was built for software: StarExec