Loading...
Please wait, while we are loading the content...
Similar Documents
Embedding acl2 models in end-user applications.
| Content Provider | CiteSeerX |
|---|---|
| Author | Davis, Jared |
| Abstract | Abstract. Formal verification, based on mechanical theorem proving, can provide unique evidence that systems are correct. Unfortunately this promise of correctness is, for most projects, not enough to justify its high cost. Since formal models and proof scripts offer few other direct benefits to system developers and managers, the idea of formal verification is abandoned. We have developed a way to embed functions from the ACL2 theorem prover into software that is written in mainstream programming languages. This lets us reuse formal ACL2 models to develop applications with features like graphics, networking, databases, etc. For example, we have written a web-based tool for hardware designers in Ruby on top of a 100,000+ line ACL2 codebase. This is neat: we can reuse the supporting work needed for formal verification to create tools that are useful beyond the formal verification team. The value added by these tools will help to justify the investment in formal verification, and the project as a whole will benefit from the precision of formal modeling and analysis. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Formal Verification Acl2 Model End-user Application System Developer Hardware Designer Proof Script Line Acl2 Codebase Mechanical Theorem Proving Acl2 Theorem Prover Formal Acl2 Model Formal Modeling Unique Evidence Mainstream Programming Language Direct Benefit Web-based Tool High Cost Formal Model Formal Verification Team |
| Content Type | Text |
| Resource Type | Article |
