-
-
I am Dave Jing Tian, an (to-be) Assistant Professor in the Department of Computer Science at Purdue University working on system security. My research involves embedded systems, operating systems, and trusted computing. All opinions are my own.
Shoot me:
root@davejingtian.org Categories
Lab
Tags
- ABNF
- agile
- AI/ML
- Alcatel-Lucent
- android
- arp
- asn1c
- assembly
- bash
- ber
- bison
- BNF
- 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
- mate
- netbeans
- netlink
- nvidia
- OS
- overo
- Python
- relay
- security
- selinux
- sgx
- socket
- ssh
- Ubuntu
- UO
- USB
- valgrind
- x86
- x86_64
- yocto
Blog Stats
- 142,854 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
