prustiの検索結果1 - 3 件 / 3件

• あとで読む

  Prustiを使ってRustでプログラム検証をしよう

  • 25 users
  • zenn.dev/iwancof
  • テクノロジー
  • 2022/09/05

  導入に際し、ドキュメントに書いてないこととか色々あってつらかったため、軽くメモ代わりに投稿しておきます。 また、Prusti を使う最も簡単な方法は VSCode の拡張である Prusti-Assistant を使うことですが、Vimの使用を見越しコマンドだけで使えるようにアレコレ設定しました。 Prusti の紹介 プログラミングにおいて、関数に対してプログラマが明示的に制約を課すことはよくあります。 例えば、次のような単純な関数 max を考えます。 fn max(x: i32, y: i32) -> i32 { let result = if x > y { x } else { y }; result } さて、この関数は次のような性質を持つことが期待されます。 resultはx以上かつy以上 resultはxまたはy そういった情報は多くの場合ライブラリのドキュメントなどに書い

  • Rust
  • testing
  • techfeed
  • プログラム

  
• あとで読む

  GitHub - viperproject/prusti-dev: A static verifier for Rust, based on the Viper verification infrastructure.

  • 6 users
  • github.com/viperproject
  • テクノロジー
  • 2022/09/11

  Prusti is a prototype verifier for Rust that makes it possible to formally prove absence of bugs and correctness of code contracts. Internally, Prusti builds upon the Viper verification infrastructure. By default Prusti verifies absence of integer overflows and panics, proving that statements such as unreachable!() and panic!() are unreachable. Overflow checking can be disabled with a configuratio

  • Rust

  
• あとで読む

  Prusti

  • 3 users
  • www.pm.inf.ethz.ch
  • テクノロジー
  • 2022/09/11

  Prusti is an automated program verifier for Rust, based on the Viper infrastructure. It leverages Rust's strong type guarantees to simplify the specification and verification of Rust programs. Formal verification of system software is notoriously difficult and requires complex specifications and logics (such as separation logic) to reason about pointers, aliasing, and side effects on mutable state

  • Rust
  • language