使用 Homebrew, dnf, MacPorts, Nix, pacman, zypper 安装 stp

项目链接

• 主页
• 仓库
• 上游文档
• 软件包管理器页面

命令和别名

• stp
• stp_simple

项目历史

The official AUTHORS file gives STP a begin date of November 2005 and names Vijay Ganesh as primary author and project leader, with early Stanford involvement from David L. Dill and later significant work by Trevor Hansen and others.

The official documentation ties STP to the CAV 2007 paper 'A Decision Procedure for Bit-Vectors and Arrays' and the CCS 2006 EXE paper, placing the project in the symbolic execution and automated bug-finding research lineage.

采用历史

STP's README describes constraints from program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and other applications as its intended workload.

The supplied package facts list STP in Homebrew, Fedora, MacPorts, Nix, Arch, and openSUSE packaging, reflecting its role as an installable solver dependency for research tools and formal-methods stacks.

使用方式

The README recommends SMT-LIB2 as the common input format and shows direct CLI usage as stp myproblem.smt2. The docs also show library and Python usage, but the package-manager-facing executable remains the solver CLI.

Users care about STP when they need a bitvector/array solver that fits into scripts, test generators, fuzzers, model checkers, or symbolic execution systems.

为什么软件包爱好者会关心

STP is package-nerd relevant because solver availability is often the difference between a formal-methods tool working out of the box and becoming a hand-built research dependency. A packaged stp executable makes SMT workflows reproducible in CI and on developer machines.

It also illustrates a classic dependency category in developer package managers: a small command-line binary with deep academic roots, used indirectly by larger verification systems.

时间线

• 2005-11: STP project begin date in AUTHORS.
• 2006: EXE paper appears in CCS and is listed by STP documentation as a basis for the project.
• 2007-07: Ganesh and Dill bitvector/array decision-procedure paper appears at CAV.
• 2013: AUTHORS file lists Dan Liew and Khoo Yit Phang as current contributors beginning in 2013.

Related projects

• STP's documentation names SMT-LIB2 as the recommended input format because it is parsed by modern bitvector solvers.
• The project builds against SAT/SMT ecosystem components such as MiniSat, and the README presents Homebrew as one supported installation path.

来源

• https://github.com/stp/stp#readme
• https://github.com/stp/stp/blob/master/AUTHORS
• https://stp.readthedocs.io/
• source_facts.package-manager