-
-
I am Dave, a PhD candidate in the Department of Computer & Information Science & Engineering (CISE) at the University of Florida. I am a founding member of FICS (Florida Institute for Cybersecurity) Research. My research involves system infrastructure, security and storage. I am interested in Linux kernel hacking, compilers and machine learning stuffs. I also play guitars though not professionally when I am tired of coding:)
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
- 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
- netstat
- nvidia
- OS
- overo
- Python
- relay
- security
- selinux
- sgx
- socket
- ssh
- Ubuntu
- UO
- USB
- valgrind
- x86
- x86_64
- yocto
Blog Stats
- 134,744 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
