STP

STP: The Simple Theorem Prover. STP is a constraint solver for the theory of quantifier-free bitvectors that can solve many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers. Features: Easy to embed or run standalone; Bindings for C, C++, and Python; Supports multiple query input formats; Open source and MIT licensed.


References in zbMATH (referenced in 41 articles , 1 standard article )

Showing results 1 to 20 of 41.
Sorted by year (citations)

1 2 3 next

  1. Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
  2. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  3. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  4. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  5. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  6. Julliand, J.; Kouchnarenko, O.; Masson, P. A.; Voiron, G.: Test generation from event system abstractions to cover their states and transitions (2018)
  7. Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
  8. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  9. Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
  10. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  11. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)
  12. Rusu, Vlad; Arusoaie, Andrei: Executing and verifying higher-order functional-imperative programs in Maude (2017)
  13. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  14. John, Ajith K.; Chakraborty, Supratik: A layered algorithm for quantifier elimination from linear modular constraints (2016)
  15. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  16. Liang, Jia Hui; Ganesh, Vijay; Poupart, Pascal; Czarnecki, Krzysztof: Learning rate based branching heuristic for SAT solvers (2016)
  17. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  18. Song, Ling; Huang, Zhangjie; Yang, Qianqian: Automatic differential analysis of ARX block ciphers with application to SPECK and LEA (2016)
  19. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
  20. Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad: Symbolic execution based on language transformation (2015)

1 2 3 next