Loading...
Please wait, while we are loading the content...
Similar Documents
Electronic Communications of the EASST Volume X ( 2010 ) Proceedings of the 10 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2010 ) Integrating Automated and Interactive Theorem Proving in Type Theory
| Content Provider | Semantic Scholar |
|---|---|
| Author | Kanso, Karim Setzer, Anton |
| Copyright Year | 2010 |
| Abstract | We introduce an approach of integrating automated theorem proving techniques into the interactive theorem prover Agda. Our approach is generic and flexible, and can be combined with dependently typed programming. We have implemented the special cases of SAT solving and CTL model checking. The tool has been used for verifying the correctness of railway interlocking systems. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.swan.ac.uk/~csetzer/articles/kansoSetzerAvocs2010.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |