The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4

Author： Gordon Michael   Kaufmann Matt   Ray Sandip  

Publisher： Springer Publishing Company

ISSN： 0168-7433

Source： Journal of Automated Reasoning, Vol.47, Iss.1, 2011-06, pp. : 1-16

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

Related content

Partial Functions in ACL2

By Manolios Panagiotis   Moore J Strother  

Journal of Automated Reasoning, Vol. 31, Iss. 2, 2003-01 ,pp. : 107-127

Springer Publishing Company

Access to resources Recommend Favorite

A First-Order Syntax for the -Calculus in Isabelle/HOL using Permutations

By Rockl C.  

Electronic Notes in Theoretical Computer Science, Vol. 58, Iss. 1, 2004-01 ,pp. : 1-17

Elsevier

Access to resources Recommend Favorite

Using Isabelle/HOL to Verify First-Order Relativity Theory

By Stannett Mike   Németi István  

Journal of Automated Reasoning, Vol. 52, Iss. 4, 2014-04 ,pp. : 361-378

Springer Publishing Company

Access to resources Recommend Favorite

Theory Extension in ACL2(r)

By Gamboa R.   Cowles J.  

Journal of Automated Reasoning, Vol. 38, Iss. 4, 2007-05 ,pp. : 273-301

Springer Publishing Company

Access to resources Recommend Favorite

Reasoning about orchestrations of web services using partial correctness

By Stewart Alan   Gabarro Joaquim   Keenan Anthony  

Formal Aspects of Computing, Vol. 25, Iss. 6, 2013-11 ,pp. : 833-846

Springer Publishing Company

Access to resources Recommend Favorite