-
Notifications
You must be signed in to change notification settings - Fork 8
FindBugsExplanation
Static checkers like FindBugs check for programming problems beyond syntactic code style checking. FindBugs is a configurable bytecode-level checker that analyzes code for common programming errors. FindBugs does not use a formal semantics or a theorem prover; its checks are entirely based upon the structure of Java bytecode.
In the Mobius PVE, we have "tuned" FindBugs to perform those checks that complement and support writing code which is verifiable using MOBIUS verification tools. In other words, if a program passes the Mobius PVE pre-configured static checkers, it is more amenable to formal verification.
Each check that is enabled in FindBugs has been evaluated and objectively analyzed to determine if it should be enabled or disabled for verification-centric programming. This evaluation is ongoing as new checks become available as FindBugs evolves.
Version: 2 Time: Fri Mar 28 12:05:56 2008 Author: dcochran (dcochran) IP: 193.1.132.32