Titlebook: Higher Order Logic Theorem Proving and Its Applications; 6th International Wo Jeffrey J. Joyce,Carl-Johan H. Seger Conference proceedings 1

浮浅

书目名称Higher Order Logic Theorem Proving and Its Applications影响因子(影响力)




书目名称Higher Order Logic Theorem Proving and Its Applications影响因子(影响力)学科排名




书目名称Higher Order Logic Theorem Proving and Its Applications网络公开度




书目名称Higher Order Logic Theorem Proving and Its Applications网络公开度学科排名




书目名称Higher Order Logic Theorem Proving and Its Applications被引频次




书目名称Higher Order Logic Theorem Proving and Its Applications被引频次学科排名




书目名称Higher Order Logic Theorem Proving and Its Applications年度引用




书目名称Higher Order Logic Theorem Proving and Its Applications年度引用学科排名




书目名称Higher Order Logic Theorem Proving and Its Applications读者反馈




书目名称Higher Order Logic Theorem Proving and Its Applications读者反馈学科排名

神秘

Mechanizing a programming logic for the concurrent programming language microSR in HOL,en to be sound within HOL. The logic we derived allows one to reason and state formal assertions about concurrently executing processes that do not share any data objects, but communicate through shared channels.

TAIN

Reasoning with the formal definition of standard ML in HOL, The correctness of the representation is demonstrated by the derivation of several important language properties, including determinacy. A symbolic evaluator to assist in proving properties of Standard ML program fragments is also described. Some sample applications of the theory in the area of program verification are given.

Vldl379

朋党派系

The HOL-Voss system: Model-checking inside a general-purpose theorem-prover,pproach. We illustrate the use of this extension with three examples, namely, the formal verification of a 32-bit adder, an 8-bit by 8-bit multiplier and the MAJORLOGIC block of the Viper microprocessor.

decipher

元音

FOLLY

惊奇

0302-9743 s 40 papers, including an invited paper by David Parnas, McMaster University, Canada, entitled "Some theorems we should prove".978-3-540-57826-0978-3-540-48346-5Series ISSN 0302-9743 Series E-ISSN 1611-3349

低位的人或事