crosshair
latest

Contents:

  • Introduction
  • Get Started
  • The Details: Contracts
  • The Details: cover
  • The Details: diffbehavior
  • Kinds of Contracts
  • Hints for Your Classes
  • IDE Integrations
  • Case Studies
  • Limitations
  • Plugins
  • How Does It Work?
  • How Can I Help?
  • Related Work
  • Contributing
  • Changelog
crosshair
  • »
  • Related Work
  • Edit on GitHub

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)

Next Previous

© Copyright . Revision 14e2a77c.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
stable
Downloads
On Read the Docs
Project Home
Builds