fixedpoint.jp




2015/03/27

Microsoft Research の Z3 Theorem Prover がオープンソースに

これまで学術目的に限り自由に利用できていた Z3 Theorem Prover のライセンスが変更され MIT License になりました: https://news.ycombinator.com/item?id=9272275

そのプロジェクトも Codeplex から GitHub に移行しています。

Z3 は SMT solver であり、Microsoft が開発している各種検証ツールの基盤として利用されている実用的なものです。クロスプラットフォームであり、C/C++ や .NET、Java、Python の API があります。その実装は効率を高めるための工夫が凝らされており、また quantifier を含む問題も制限付きながら扱えるそうです: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

#permalink

2015/03/17

SRFI 終了?

comp.lang.scheme にて Michael Sperber 氏が srfi.schemers.org のメンテナンスをやめるというメッセージを送っています: https://groups.google.com/forum/#!topic/comp.lang.scheme/GbqFPWRL4Xw

その説明によると、これまで氏の個人的なサーバーで web サーバーとメーリングリストを運営していたそうです。1998年以来続いてきた Scheme のライブラリの提案や仕様拡張、およびその議論の記録がこのまま失われるとは考えられません。おそらく今後別の体制で継続されるものと期待されます。

#permalink

2015/03/09

静的解析ツールで LibreOffice のバグを検出、およびその逆

LibreOffice プロジェクトではその C++ コードを様々なツールを使って日々解析しています: Re: Questions about code reviews and static analysis tools for TU Delft research

中でも Coverity による静的解析はこれまで多くの問題を検出してきただけでなく、日常的に開発ブランチをチェックするサービスが提供されているため日々利用されています。

一方、最近 PVS-Studio という静的解析ツールの開発元が LibreOffice のコードを解析したという記事が公開されています: LibreOffice Project's Check

その中で明らかな typo や条件判定の間違いなどが数多く挙げられています。この記事が公開されてすぐ LibreOffice の開発者たちは修正し始めています(a59848c9999f655342db4c67e3dc390cc083e511 など)。

特筆するべきは、Coverity その他で検出された問題を既にほとんど修正しているにも関わらず、PVS-Studio が別種の問題を見つけることができたということです。これは、多様な静的解析ツールを駆使すれば同種のツールのみを用いる場合よりも効果が期待できることを示しています。また同時に、上のページの結論として

Although the number of errors, defects, and slip-ups discussed in this article is, as usual, great, the LibreOffice project's code is still very high-quality. And it does bear the evidence of being regularly checked by Coverity, which indicates the authors' serious approach to the development. The number of bugs found by PVS-Studio is pretty small for such a large project like LibreOffice.

とされており、LibreOffice コードの品質は既にかなり高いようです。

興味深いことに、PVS-Studio の開発元は逆の実験もしています。すなわち、巨大なコードベースを持つ LibreOffice を解析することで PVS-Studio のバグを見つけています: Bugs Found by LibreOffice in PVS-Studio

#permalink

Archives

2015: Feb

2014: Dec / Nov / Oct / Aug / Apr / Mar / Feb / Jan

2013: Dec / Nov / Oct / Sep / Aug / Jun / May / Apr / Mar

2012: Nov / Oct / Sep / Jul / Jun / May / Mar / Feb / Jan

2011: Dec / Nov / Oct / Sep / Jul / Jun / Apr / Mar / Feb / Jan

2010: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2009: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2008: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2007: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2006: Dec / Nov / Oct / Sep


© 2006-2015 fixedpoint.jp