Name
Abstract | ||
|---|---|---|
We implement a large Isabelle/HOL repository of algebras for application in modelling computing systems. They subsume computational logics such as dynamic and Hoare logics and form a basis for various software development methods. Isabelle has recently been extended by automated theorem provers and SMT solvers. We use these integrated tools for automatically proving several rather intricate refinement and termination theorems. We also automate a modal correspondence result and soundness and relative completeness proofs of propositional Hoare logic. These results show, for the first time, that Isabelle's tool integration makes automated algebraic reasoning particularly simple. This is a step towards increasing the automation of formal methods. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-24559-6_41 | ICFEM |
Keywords | Field | DocType |
algebraic method,formal method,large isabelle,smt solvers,automated theorem provers,propositional hoare logic,integrated tool,hol repository,hoare logic,computational logic,algebraic reasoning | HOL,Computational logic,Programming language,Computer science,Hoare logic,Theoretical computer science,Automation,Mathematical proof,Boolean algebra,Formal methods,Soundness | Conference |
Volume | ISSN | Citations |
6991 | 0302-9743 | 11 |
PageRank | References | Authors |
0.56 | 23 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Walter Guttmann | 1 | 196 | 16.53 |
| Georg Struth | 2 | 641 | 53.76 |
| Tjark Weber | 3 | 215 | 19.33 |