Zobrazeno 1 - 10
of 50
pro vyhledávání: '"Michael J. C. Gordon"'
Autor:
Tom Melham, Michael J. C. Gordon, Konrad Slind, Richard J. Boulton, Graham Robinson, Louise A. Dennis, Graham Collins, Michael Norrish
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783540672821
TACAS
TACAS
The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treated as components. A system incorporating
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::61987c8dfd9f90ad2d365e86f13cbe30
https://ora.ox.ac.uk/objects/uuid:b21b72e3-93b9-49ae-8386-b7879b5558cd
https://ora.ox.ac.uk/objects/uuid:b21b72e3-93b9-49ae-8386-b7879b5558cd
Publikováno v:
Journal of Automated Reasoning. 47:1-16
We present a case study illustrating how to exploit the expressive power of higher-order logic to complete a proof whose main lemma is already proved in a first-order theorem prover. Our proof exploits a link between the HOL4 and ACL2 proof systems t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::946f2648ba9c55e5b3aa00ddaca1c1f3
https://doi.org/10.1007/s10817-010-9169-y
https://doi.org/10.1007/s10817-010-9169-y
Autor:
Magnus O. Myreen, Michael J. C. Gordon
Publikováno v:
Electronic Notes in Theoretical Computer Science. 240:185-200
This paper presents a new proof-assistant based approach to program verification: programs are translated, via fully-automatic deduction, into tail-recursive function defined in the logic of a theorem prover. This approach improves on well-establishe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::171812d1a524bd39c9be0f074029613c
https://doi.org/10.1016/j.entcs.2009.05.052
https://doi.org/10.1016/j.entcs.2009.05.052
Publikováno v:
Formal Aspects of Computing. 19:343-362
A compiler from a synthesisable subset of higher order logic to clocked synchronous hardware is described. It is being used to create coprocessors for cryptographic and arithmetic applications. The compiler automatically translates a function f defin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1203451f913f3c2c42cf4d134f5d51ed
https://doi.org/10.1007/s00165-007-0028-5
https://doi.org/10.1007/s00165-007-0028-5
Publikováno v:
Electronic Notes in Theoretical Computer Science. 145:27-43
A compiler that automatically translates recursive function definitions in higher order logic to clocked synchronous hardware is described. Compilation is by mechanised proof in the HOL4 system, and generates a correctness theorem for each function t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f8e56f09e8494f78ba72507149114e13
Autor:
Michael J. C. Gordon
Publikováno v:
Formal Aspects of Computing. 15:406-421
The Accellera organisation selected Sugar, IBM’s formal specification language, as the basis for a standard to ‘drive assertion-based verification’ in the electronics industry. Sugar combines regular expressions, Linear Temporal Logic (LTL) and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7dc087533e9a87a6d03fa0f143993d68
https://doi.org/10.1007/s00165-003-0014-5
https://doi.org/10.1007/s00165-003-0014-5
Autor:
Michael J. C. Gordon
Publikováno v:
LMS Journal of Computation and Mathematics. 5:56-76
A generalisation of Milner's ‘LCF approach’ is described. This allows algorithms based on binary decision diagrams (BDDs) to be programmed as derived proof rules in a calculus of representation judgements. The derivation of representation judgeme
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f443e90efcf467f16ee86c17ef073671
https://doi.org/10.1112/s1461157000000693
https://doi.org/10.1112/s1461157000000693
Autor:
Michael J. C. Gordon
Publikováno v:
The Computer Journal. 45:27-36
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1478084b83ff00fd5b5a46ebba823757
https://doi.org/10.1093/comjnl/45.1.27
https://doi.org/10.1093/comjnl/45.1.27
Publikováno v:
Information and Software Technology. 37:269-276
A simple ‘shallow’ semantic embedding of the Z notation into the higher order logic, as supported by the HOL theorem proving system, is presented. Z is typically used for human-readable formal specification whereas HOL is used for machine-checked
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4d38347efa7e7536747bb27b700f10d2
https://doi.org/10.1016/0950-5849(95)99362-q
https://doi.org/10.1016/0950-5849(95)99362-q
Publikováno v:
Design and Verification of Microprocessor Systems for High-Assurance Applications ISBN: 9781441915382
Design and Verification of Microprocessor Systems for High-Assurance Applications
Design and Verification of Microprocessor Systems for High-Assurance Applications
The ARM verification project started in 2000 with the aim of seeing whether existing mechanised formal specification and verification methods could be applied to a commercial off-the-shelf processor. After succeeding in formally verifying that a mode
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::89c7b4e44bf3f08d5bff3cd8469d5ca8
https://doi.org/10.1007/978-1-4419-1539-9_8
https://doi.org/10.1007/978-1-4419-1539-9_8