Related Work¶
Related Topics and Tools:
- dependent types, refinement types
CrossHair aims to provide many of the same capabilities as these advanced type systems. CrossHair is easier to learn (because it is just python), but is incomplete. It can’t always tell you whether a condition holds.
- design by contract
Unlike most tools for contracts, CrossHair attempts to verify pre-conditions and post-conditions before you run them.
- fuzz testing, QuickCheck, property testing, Hypothesis
CrossHair has many of the same goals as these tools. However, CrossHair uses an SMT solver to find inputs rather than the (typically) randomized approaches that these tools use.
- concolic testing
CrossHair is essentially a concolic testing system. This kind of tool sits in a middle ground in between property testing and formal methods.
- formal methods, Nagini
CrossHair is good at finding counterexamples, but cannot generally prove that properties hold. Formal method tools can help you do that. For example, Nagini, is a verifier for Python programs.
The main downside of full verification is that you’ll need to understand a bit about how the verifier works and may need to guide it with additional information like loop invariants and termination proofs.
- SMT solvers
SMT solvers power many of the tools listed here. CrossHair uses Z3.
- angr, klee
Symbolic execution of binary code. Unlike these tools, CrossHair models the semantics of Python directly.
- PyExZ3, pySim, PEF
These projects take approaches are very similar to CrossHair, and are in varying states of completeness. CrossHair is generally more prescriptive or product-like than these tools.
Work Involving CrossHair:
Andrea Veneziano & Samuel Chassot. 2022. SVSHI: Secure and Verified Smart Home Infrastructure. (see also the github repo and in particular the docs on verification)
Loïc Montandon. 2022. Exhaustive symbolic execution engine for verifying Python programs.
Aymeri Servanin. 2022. Extending the verification of SVSHI applications with time-sensitive constraints.
Jiyang Zhang, Marko Ristin, Phillip Schanely, Hans Wernher van de Venn, Milos Gligoric. 2022. Python-by-Contract Dataset.
Shikha Mody, Bradley Mont, Jivan Gubbi, & Brendon Ng. 2022. Semantic Merge Conflict Detection. (see also the github repo)