Cited in
(only showing first 100 items - show all)- Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
- Old or heavy? Decaying gracefully with age/weight shapes
- Restricted combinatory unification
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Faster, higher, stronger: E 2.3
- Multi-dimensional interpretations for termination of term rewriting
- The CADE-26 automated theorem proving system competition -- CASC-26
- Scavenger 0.1: a theorem prover based on conflict resolution
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- Term orderings for non-reachability of (conditional) rewriting
- Synthesis of domain specific CNF encoders for bit-vector solvers
- The \textsc{SDEval} benchmarking toolkit
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- On solving quantified bit-vector constraints using invertibility conditions
- Counterexample-guided quantifier instantiation for synthesis in SMT
- The 2013 evaluation of SMT-COMP and SMT-LIB
- Learning Optimal Decision Sets and Lists with SAT
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- Performance of clause selection heuristics for saturation-based theorem proving
- Proving termination through conditional termination
- Scaling enumerative program synthesis via divide and conquer
- Incomplete SMT techniques for solving non-linear formulas over the integers
- A calculus for modular loop acceleration
- A combinator-based superposition calculus for higher-order logic
- Layered clause selection for theory reasoning (short paper)
- Selecting the selection
- Making higher-order superposition work
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- scientific article; zbMATH DE number 7359428 (Why is no real title available?)
- Refutation-based synthesis in SMT
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- Machine learning-based restart policy for CDCL SAT solvers
- HaifaSat
- FLATA
- SMT-LIB
- TPTP
- SPASS+T
- PURRS
- PoCaB
- Satallax
- NiVER
- Zeno
- Asparagus
- RunLim
- Runsolver
- CVC4
- Bloqqer
- Aligators
- Eldarica
- CoLoR
- MU-TERM
- TPDB
- GQML
- MetTeL
- Kaluza
- Easychair
- Beagle
- Ctrl
- Saucy
- FAST
- Leo-III
- HordeQBF
- MPIDepQBF
- OpenSMT2
- EFSMT
- DISCOUNT
- JST
- RADA
- ConCon
- FMLtoHOL
- nanoCoP
- Nagoya Termination Tool
- QBFEVAL
- LoAT
- H-PILoT
- Scavenger
- RAHFT
- abcdSAT
- AIGSolve
- CAQE
- MapleSAT
- CoCoWeb
- CO3
- Cops
- AVATAR
- HQSpre
- MadMax
- Lambda Free RPOs
- CoqHammer
- ZRes
- FlashMeta
- Stern-Brocot Tree
- lbtt
- Twee
- SMTS
- TRANSIT
- Zipperposition
- cnf2aig
- TcT
This page was built for software: StarExec
