-
-
I am Dave (Jing) Tian, an Associate Professor in the Department of Computer Science at Purdue University working on system security. My research involves embedded systems, operating systems, trusted and confidential computing, and hardware security. All opinions are my own.
Shoot me:
root@davejingtian.org Categories
Tags
- ABNF
- agile
- AI/ML
- Alcatel-Lucent
- android
- arp
- asn1c
- assembly
- bash
- ber
- bison
- BNF
- build
- C
- CentOS
- CIS122
- Coverity
- crypto
- csv
- cuda
- DCA
- ddclient
- debugfs
- DH
- Diffie-Hellman
- drd
- drig
- elixir
- fedora
- fedup
- flex
- fsck
- gcc
- gdb
- GFW
- git
- github
- gnome
- gprof
- gpu
- guitar
- gumstix
- helgrind
- intel
- itevad
- Java
- jmgsim
- JVM
- kenai
- kernel
- kill
- ksh
- kvm
- ld
- Linux
- list
- netbeans
- netlink
- nvidia
- OS
- overo
- Python
- relay
- security
- selinux
- sgx
- socket
- ssh
- Ubuntu
- UO
- USB
- valgrind
- x86
- x86_64
- yocto
Blog Stats
- 275,423 hits
-
All blogs on this website are licensed under a Creative Commons Attribution 4.0 International License. -
-
-
Tag Archives: HOL
A paper review – seL4: Formal Verification of an OS kernel
Paper review for – seL4: Formal Verification of an OS Kernel daveti@cs.uoregon.edu Dec 10, 2013 How could we guarantee the code we are running is right? Even after different and long-time testing, we have yet not been so sure that … Continue reading →
Posted in Embedded System, OS, Programming, Security
|
Tagged C, Haskell, HOL, Isabelle, seL4
|
Leave a comment
davejingtian.org 