wdv4758h-notes
latest
  • 演算法與資料結構
  • ADT (Abstract Data Type)
  • 演算法相關概念
  • Big O Notation
  • Books
  • Cache
  • Cache Friendly Algorithms
  • Dict
  • Float to String
  • Heap （堆）
  • 演算法與資料結構
  • Inverse Square Root
  • Lock
  • Meta Algorithm
  • Misc
  • Probabilistic Data Structure
  • Random Number Generator
  • 演算法
  • Sorting
  • String to Float
  • Substring Searching
  • Android
  • Android Emulator
  • Android Images
  • Anbox - 在 GNU/Linux 上執行 Android 系統
  • Android Apps
  • Android’s Binder
  • Android boot
  • Android Cheat Sheet
  • Android Process Crash Debug
  • Android CTS (Compatibility Test Suite)
  • Google Project Butter
  • 硬體抽象層 (HAL) (Hardware Abstraction Layer)
  • Android - init
  • 安裝新 Android
  • Android Kernel
  • libhybris
  • Linux environment on Android
  • Android NDK
  • 移植到新硬體 (Porting to new Hardware)
  • Android Profiling
  • 重刷 Android 版子
  • SurfaceFlinger
  • ARM Server
  • ARM Introduction
  • Python - Need For Speed
  • 用 Travis CI 自動化發佈 reStructuredText 到 GitHub Pages 上
  • CPU & ISA
  • Assembly Cheat Sheet
  • SHA Extensions
  • libuv
  • Binary Instrumentation
  • Reference
  • Blog
  • Artificial Neural Network
  • History
  • Reference
  • Installation
  • Cross Compile
  • Control
  • Performance Testing
  • Reference
  • C++ 繼承
  • Virutal Function
  • C++11 - override & final
  • Ref
  • Basic Linux IPC
  • D-Bus
  • kdbus
  • Web Storage V.S. Cookies
  • Web Storage
  • Reference
  • bzImage
  • initramfs
  • zlib
  • Linux Standard Base (LSB)
  • Filesystem Hierarchy Standard (FHS)
  • Stack & Heap
  • Common Memory Problem
  • Debugger
  • RAII (Resource Acquisition Is Initialization)
  • Ownership
  • Garbage Collection
  • Cases
  • Allocator Implementations
  • Debugging Data Format
  • Reference
  • Install
  • Linux
  • Mac OS X
  • Browser
  • Introduction
  • Reference
  • Introduction
  • Tutorial
  • 額外紀錄
  • Reference
  • Introduction
  • Hello World
  • PyStone
  • PyBench 2.0
  • Richards
  • 總結
  • Reference
  • Introduction
  • Tutorial
  • Celery with non-Python
  • Frequently Asked Questions
  • Reference
  • ch 14-1 - functional programming
  • ch 14-4 Ruby with C
  • ch 14-5 Open Source
  • ch 2-5 Duck Typing
  • ch 8 Regular Expression
  • ch 9-1 Integer
  • ch 9-2 Float
  • Install QEMU
  • Create Image
  • Install OS from bootable ISO
  • QEMU with KVM
  • Syntax
  • Closure 和外部變數
  • “move” closures
  • Closure implementation
  • closures as arguments
  • returning closures
  • Reference
  • Solution 1
  • Solution 2
  • Solution 3
  • Solution 4
  • Todo
  • Intro.
  • Ch5 - Boundary Value Testing
  • Ch6 - Equivalence Class Testing
  • Ch7 - Decision Table-based Testing
  • Ch8 - Path Testing
  • Ch9 - Data Flow Testing
  • Ref
  • [Ｏ] Big Number 支援？
  • [Ｏ] First-class function 支援？
  • [Ｏ] map / reduce / filter 之類的東西？
  • [Ｏ] Option type (maybe type) ?
  • [Ｏ] OOP (object-oriented programming)？
  • [Ｏ] Type Inference
  • [Ｏ] 高度的 Memory Control？
  • [－] REPL？
  • [？] 預設提供的 Sort Algorithm 是啥？
  • [Ｏ] Regular Expression 支援？
  • [Ｏ] FFI (Foreign Function Interface)？
  • [Ｏ] Import third party library？
  • [Ｏ] Native Threading Support？
  • [Ｘ] Garbage Collection？
  • [Ｏ] Format String？
  • [Ｏ] Ownership？
  • Third Party
  • vdpau
  • libva
  • Chromium
  • Reference
  • 方法 1 : 在 insert mode 快速貼上
  • 方法 2 : 在 normal mode 快速貼上
  • 其他應用 - 從 Vim 裡複製到 system clipboard
  • 其他 Vim registers
  • 參考資料
  • libinput
  • 近況
  • Users
  • Reference
  • 瀏覽器相關
  • CDM
  • Chrome
  • CSS
  • How Browser Work
  • WebExtensions
  • Firefox
  • Firefox 設定
  • HTML
  • Issues
  • 隱私和個資
  • Service Worker
  • Servo
  • WebAssembly
  • Build System
  • CMake
  • GYP
  • Makefile
  • Meson
  • C
  • C
  • C Cheat Sheet
  • Exceptions in C
  • Some C’s features
  • GLib
  • GNU Extension
  • Internal and External Linkage in C
  • mmap
  • pragma once
  • pragma weak
  • 相關資源
  • Undefined Behavior
  • 256 color
  • CLI/TUI 工具
  • autossh
  • Bash
  • Basic System Utils
  • BusyBox - 人人都該備一個在身邊的執行檔
  • 晶片讀卡機
  • curl
  • date
  • du
  • file - 檢查檔案種類
  • find
  • hwclock
  • Input Method
  • Installer
  • Some Basic Tools
  • IRC
  • xmodmap
  • setxkbmap
  • lsblk - 顯示裝置資訊
  • Office
  • Remote Desktop
  • rsync
  • sed
  • Shell
  • SSH Config
  • sudo
  • Sway
  • tar
  • test 指令
  • timedatectl
  • Tips
  • Tmux
  • 工具
  • xargs
  • 雲端服務 (Cloud Service)
  • 編譯器
  • Compiler Autotuning
  • Branch Prediction Hint
  • Clang Options
  • Clang Tools
  • Code Generation
  • Compiler and Learning
  • Compiler Options
  • LLVM - compiler-rt
  • Computed goto
  • Cross Compile
  • crt
  • Environment
  • GCC Plugins
  • GPGPU
  • Incremental Compilation
  • 編譯器
  • Jump Threading
  • Legalization
  • LLVM
  • Android With LLVM
  • LLVM & CUDA
  • LLVM 輔助測試
  • LLVM IR
  • LLVM & Python
  • LLVM to VHDL/Verilog
  • Name Mangling
  • Obfuscator
  • Objdump
  • Use Compiler To Help Porting
  • Compiler Resource
  • SSA
  • Streaming Compilation
  • Talks
  • TCG IR - Tiny Code Generator
  • 轉譯器 (Transpiler) (Source-to-Source Compiler)
  • 壓縮
  • 壓縮入門
  • JPEG Compression
  • PNG Compression
  • 資料壓縮相關資源
  • 電腦視覺 (Computer Vision)
  • SIFT
  • Background Subtraction
  • 電腦視覺相關書籍
  • Image Segmentation
  • Object Detection
  • Object Recognition
  • Object Tracking
  • Panorama (Image Stitching)
  • Super Resolution
  • Video Tracking
  • Visual Question Answering
  • Concurrency
  • Lock
  • 名詞釐清
  • Container
  • chroot
  • Docker
  • FreeBSD Jail
  • Linux Containers (LXC)
  • CI (Continouse Integration)
  • Buildbot
  • Continuous Integration
  • Concourse
  • Drone
  • Github Actions
  • Jenkins
  • Travis CI
  • Workflow Pipeline
  • 64 Bits Problem
  • C++
  • SFINAE (Substitution Failure Is Not An Error)
  • std::array
  • C++ & Assembly
  • C++ Bit Field
  • C++17
  • C++ Concepts
  • C++ const
  • Copy Elision
  • C++ Coroutine
  • C++ Core Guidelines
  • CRTP (Curiously Recurring Template Pattern)
  • C++ Constructors & Destructors
  • Design Pattern
  • C++ Documentation
  • Experimental
  • explicit specifier
  • Expression Templates
  • Forward Declaration
  • C++ History
  • 繼承 (Inheritance)
  • Initialization
  • lambda function
  • Macro
  • C++ Misc
  • C++ Optimizations
  • Optional
  • C++ - Parallel
  • Perfect Forwarding
  • Pimpl
  • Qt
  • C++ REPL
  • C++ Resource
  • RVO (Return Value Optimization)
  • About size_t and ptrdiff_t
  • Smart Pointer
  • Standard Library Implementation
  • static
  • C++ STL
  • String Optimization
  • Temporary Objects
  • C++ Testing
  • C++ Thread
  • Todo
  • 型別轉換 (Type Conversion)
  • 型別推斷 (Type Deduction)
  • C++ Value Category
  • C++ Videos
  • CPU & ISA
  • Assembly Cheat Sheet
  • SHA Extensions
  • Blowfish
  • Elliptic Curve
  • Crypto
  • SHA (Secure Hash Algorithm)
  • 資料庫 (Database)
  • CockroachDB
  • Raft Consensus Algorithm
  • Graph Database
  • LevelDB
  • MariaDB
  • Materialized Views
  • MongoDB
  • MySQL
  • Database
  • Redis
  • Database (資料庫)
  • RocksDB
  • SQL (Structured Query Language)
  • SQLite
  • TiDB
  • 除錯相關 (Debugging)
  • FlameScope
  • GDB
  • Debugger for JavaScript
  • Debugging a Kernel
  • PDB - Python Debugger
  • Resource
  • rr - record and replay framework
  • strace
  • 文件 (Documentation)
  • LaTeX 教學
  • reStructuredText
  • Sphinx
  • E-Book
  • EPUB
  • 編輯器
  • Emacs
  • 嵌入式 (Embedded)
  • BSP (Board Support Package)
  • FPGA
  • Embedded Resource
  • STM32
  • 字型相關 (Fonts)
  • 形式驗證 (Formal Verification)
    • SMT
    • 案例探討
      • seL4
      • CompCert C compiler
      • Galois, Inc
        • Software Analysis Workbench
    • 參考
  • 朋友的筆記
  • 遊戲 (Game)
  • Emulators
  • 遊戲引擎 (Game Engine)
  • Real-time Strategy Games
  • Games Resource
  • Roguelike
  • Role-playing Games (RPG)
  • 守塔 (Tower Defense)
  • Windows Game on Linux
  • ArrayFire
  • Boost.Compute
  • GPGPU with Kernel
  • SPIR-V
  • 圖像處理 (Graphics)
  • Cairo - 跨平台二維向量繪圖
  • DRI (Direct Rendering Infrastructure)
  • GLSL - OpenGL Shading Language
  • Graphic
  • Linux Graphics
  • Mesa - 跨平台三維繪圖
  • OpenGL
  • Graphic Resource
  • VirtualGL
  • Vulkan
  • GUI
  • GTK
  • Qt
  • 硬體相關 (Hardware)
  • Hardware & Programming
  • 耳機 (Headphone)
  • Hardware’s History
  • Kindle
  • Resource
  • RISC-V
  • 相關資源
  • 機器學習 (Machine Learning)
  • Cheat Sheet
  • 數學相關
  • 計算機
  • 誤差
  • 數學相關套件 (Math Libraries)
  • 線性代數 （Linear Algebra）
  • Math on Web
  • Math
  • W^X (Write XOR Execute)
  • Allocator
  • AddressSanitizer Algorithm
  • Kernel Memory Management
  • Memory
  • Memory Allocator - Under The Hood
  • Memory Hardware
  • Memory Management
  • Memory Profiler
  • Memory Profiling
  • Sanitizer
  • Stack Protection
  • Advertisement Blocker
  • Archive
  • 一些閱讀過的文章
  • 頻寬成本
  • Bio Data Format
  • Bit Hacks
  • 踩 Bug 紀錄 (從 2015-10-26 開始)
  • CAD (Computer-Aided Design)
  • Calendar
  • ChatOps
  • Cloud Message
  • Conference
  • Open Source 專案貢獻
  • Disk Encryption
  • DOT Language
  • 簡易網站建立服務
  • Esoteric Programming Language
  • Fish Shell
  • Floating Point
  • Forum
  • 臺灣自由軟體界
  • Funny Sites
  • Google OnHub
  • 十六進位浮點數（Hex Float）
  • Hexspeak
  • High Availability
  • 資訊相關歷史
  • Host Blocker
  • HTTP History
  • Images
  • 物聯網 (IoT) (Internet of Things)
  • IRC
  • Jargons
  • Keyboard
  • Linux Foundation
  • Log Analysis
  • Mail System
  • Man Page
  • Misc
  • Netflix
  • OpenAPI
  • Open House
  • Open Source Porjects I Love
  • 緣由
  • Papers
  • PDF Viewer History
  • 效能要點 (Performance)
  • Podcast
  • Project Measurement
  • proxychains
  • 資訊相關書籍出版社
  • 遠端工作 (Remote Jobs)
  • Interesting Repo
  • 資源來源
  • 逆向工程
  • 火箭
  • SAT/SMT Solver
  • Self Hosting
  • Sites
  • Software Updates
  • Statifier
  • 台灣軟體界
  • Task Execution Framework
  • Task Schedule
  • Team Collaboration
  • Todo
  • 想做的專案
  • Tools
  • Trace Code
  • 翻譯 (Translation)
  • 技術屁話
  • Turing Complete
  • Typesetting
  • 大學修過的課程
  • Unicode 解說
  • Video
  • 一些 Talk 的影片
  • Voice Simulation
  • Windows Batch
  • Working Memory
  • 多媒體 (Multimedia)
  • Audio
  • 基本概念
  • GStreamer
  • Kodi - Open Source Home Theater Software
  • Linux Sound System
  • Media Container
  • MediaInfo
  • MIDI
  • Music Player
  • OpenCV
  • PipeWire
  • 播放器
  • PTS/DTS (Presentation Time Stamp/Decode Time Stamp)
  • PulseAudio
  • SDP (Session Description Protocol)
  • Video
  • Video Quality
  • 網路相關 (Network)
  • AMQP (Advanced Message Queuing Protocol)
  • C10K
  • C10M
  • DDoS
  • Distributed
  • DNS
  • DTLS (Datagram Transport Layer Security)
  • HTTP (Hypertext Transfer Protocol)
  • ICE (Interactive Connectivity Establishment)
  • iperf - TCP/UDP/SCTP 網路效能測量
  • Microservice
  • Network Monitoring
  • MQTT (Message Queuing Telemetry Transport)
  • nanomsg
  • Network Load Balancer
  • Network Stack
  • Nginx
  • OS socket buffer
  • Proxy
  • QUIC
  • 資源
  • RPC
  • 安全性檢查
  • SRT (Secure Reliable Transport)
  • TCP
  • tcpdump
  • UDP
  • UPnP
  • VPN
  • WebSocket
  • WebTorrent
  • 作業系統
  • 作業系統相關歷史
  • OpenHMPP
  • OpenMP
  • Parallel
  • 平行化相關資源
  • 程式語言 (Programming Language)
  • Interpreter For Compiled Language
  • 語言效能比較
  • Python
  • Python AST
  • Python - async & await
  • Asynchronous
  • Benchmark
  • Best Practice
  • Python Compiler
  • Python’s Concurrency
  • contextlib
  • CPython
  • CPython Equality
  • CPython Extension
  • Cython
  • Debugger
  • Some Deprecated Things
  • Django
  • CPython GIL (Global Interpreter Lock)
  • Python & Hardware
  • Python - Install Packages
  • Python
  • Iterator
  • Kivy - Python on Android
  • Linter & Formatter
  • 製作 Packages
  • matplotlib
  • Nuitka
  • Numpy
  • Operator
  • Some Packages
  • Parser in Python
  • 遷移至 Python 3
  • ** operator v.s. math.pow
  • PyPI
  • PyPy
  • Python 3.5
  • Python 3.6
  • Python 3.7
  • Qt
  • Resource
  • SciPy
  • Standard Library
  • SymPy
  • Python Testing
  • Python Tips
  • virtualenv
  • yield with list comprehension
  • 量子電腦
  • RE2 - fast, safe, thread-friendly alternative to backtracking regular expression engines
  • Regular Expression
  • Regular Expression Library
  • Resource
  • Engineering Report <dv> - Week 28, 2015
  • Engineering Report <dv> - Week 29, 2015
  • Engineering Report <dv> - Week 30, 2015
  • Engineering Report <dv> - Week 31, 2015
  • Engineering Report <dv> - Week 32, 2015
  • Engineering Report <dv> - Week 33, 2015
  • Engineering Report <dv> - Week 34, 2015
  • Engineering Report <dv> - Week 35, 2015
  • Engineering Report <dv> - Week 36, 2015
  • Engineering Report <dv> - Week 37, 2015
  • Self Report <dv> - Week 53, 2015
  • Self Report <dv> - Week 54, 2015
  • Self Report <dv> - Week 55, 2015
  • Self Report <dv> - Week 56, 2015
  • Self Report <dv> - Week 19, 2016
  • Self Report <dv> - Week 20, 2016
  • Self Report <dv> - Week 21, 2016
  • Self Report <dv> - Week 22, 2016
  • Self Report <dv> - Week 23, 2016
  • Information For Your Report
  • Engineering Report <dv> - Week #, 2016
  • 機器人 (Robot)
  • Boston Dynamics
  • Farming Robot
  • Rust 相關文章
  • 搜尋引擎 (Search Engine)
  • 資訊安全相關 (Security)
  • Clickjacking
  • Security issues in JavaScript Engine
  • 資源
  • 逆向工程 (Reverse Engineering)
  • SGX (Secure Guard Extensions)
  • Security
  • Security Libs
  • SIMD
  • 運用 SIMD 來加速的演算法
  • SIMD
  • 同步 (Synchronization)
  • 測試 (Testing)
  • Chaos Engineering
  • Fuzzer
  • Test Mobile App
  • Mutation Test
  • 檢查伺服器設定
  • 版本控制 (Version Control)
  • Mercurial
  • Pijul
  • 虛擬化 (Virtualization)
  • Bareflank
  • bhyve
  • KVM
  • QEMU
  • 視覺化 (Visualization)
  • Wiki
wdv4758h-notes
  • 形式驗證 (Formal Verification)
  • Edit on GitHub

形式驗證 (Formal Verification)

目錄

  • 形式驗證 (Formal Verification)

    • SMT

    • 案例探討

      • seL4

      • CompCert C compiler

      • Galois, Inc

        • Software Analysis Workbench

    • 參考

SMT

案例探討

seL4

CompCert C compiler

Galois, Inc

Software Analysis Workbench

參考

  • Wikipedia - Formal Verification

  • Wikipedia - Formal equivalence checking

  • The Software Analysis Workbench

  • Formal Verification - jserv

Previous Next

© Copyright 2023.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
Downloads
htmlzip
On Read the Docs
Project Home
Builds