Blockchain fundamental

January 1, 1 · 6386 words · 13 min · blockchain

区块链技术与应用 1 引言 1.1 课程基本信息 参考资料： ​ 以太坊白皮书、黄皮书、源代码 ​ solidity 2 比特币 2.1 BTC密码学原理 crypto-currency 哈希 cryptographic hash function collision resistance （x!=y, but H(

Introduction to Model Checking

January 1, 1 · 3477 words · 7 min · model checking

Chapter 1 Introduction to Model Checking 摘要 A computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. 计算机辅助验证之例 The only effective way to raise the

Model Checking Chapter

January 1, 1 · 193 words · One minute · model checking

chapters of the book Each chapter of this handbook is a survey in its own right, and reflects the viewpoint, the notation, and the terminology used by the specialists in the respective research area. The handbook chapters are intended as independent introductions to the state-of-the-art research literature on specific topics rather than as chapters of a monograph. Introduction to Model Checking Temporal Logic and Fair Discrete Systems Modeling for Verification Automata Theory and Model Checking Explicit-State Model Checking Partial-Order Reduction Binary Decision Diagrams BDD-Based Symbolic Model Checking Propositional SAT Solving SAT-Based Model Checking Satisfiability Modulo Theories Compositional Reasoning Abstraction and Abstraction Refinement Interpolation and Model Checking Predicate Abstraction for Program Verification Combining Model Checking and Data-Flow Analysis Model Checking Procedural Programs Model Checking Concurrent Programs Combining Model Checking and Testing Combining Model Checking and Deduction Model Checking Parameterized Systems Model Checking Security Protocols Transfer of Model Checking to Industrial Practice Functional Specification of Hardware via Temporal Logic Symbolic Trajectory Evaluation The mu-Calculus and Model Checking Graph Games and Reactive Synthesis Model Checking Probabilistic Systems Model Checking Real-Time Systems Verification of Hybrid Systems Symbolic Model Checking in Non-Boolean Domains Process Algebra and Model Checking

Temporal logics

January 1, 1 · 1082 words · 3 min · model checking

时序逻辑和公平离散系统 Temporal Logic and Fair Discrete Systems 摘要 Temporal logics can be classified by their view of the evolution of time as either linear or branching. In the linear-time view, we see time ranging over a linear total order and executions are sequences of states. When the system has multiple possible executions (due to nondeterminism or reading input) we