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 44 articles , 1 standard article )

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

1 2 3 next

  1. de Boer, Frank S.; Bonsangue, Marcello: Symbolic execution formally explained (2021)
  2. Li, Chunxiao; Chung, Jonathan; Mukherjee, Soham; Vinyals, Marc; Fleming, Noah; Kolokolova, Antonina; Mu, Alice; Ganesh, Vijay: On the hierarchical community structure of practical Boolean formulas (2021)
  3. Trentin, Patrick; Sebastiani, Roberto: Optimization modulo the theories of signed bit-vectors and floating-point numbers (2021)
  4. Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
  5. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  6. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  7. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  8. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  9. Julliand, J.; Kouchnarenko, O.; Masson, P. A.; Voiron, G.: Test generation from event system abstractions to cover their states and transitions (2018)
  10. Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
  11. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  12. Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
  13. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  14. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)
  15. Rusu, Vlad; Arusoaie, Andrei: Executing and verifying higher-order functional-imperative programs in Maude (2017)
  16. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  17. John, Ajith K.; Chakraborty, Supratik: A layered algorithm for quantifier elimination from linear modular constraints (2016)
  18. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  19. Liang, Jia Hui; Ganesh, Vijay; Poupart, Pascal; Czarnecki, Krzysztof: Learning rate based branching heuristic for SAT solvers (2016)
  20. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)

1 2 3 next