Jean Yang
- Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO) (Amsterdam, the Netherlands, 2006), volume 4111. Google Scholar
Digital Library
- Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D. An approach to systems verification. J. Autom. Reason. 5, 4 (1989), 411--428. Google ScholarDigital Library
- Chen, J., Hawblitzel, C., Perry, F., Emmi, M., Condit, J., Coetzee, D., Pratikakis, P. Type-preserving compilation for large-scale optimizing object-oriented compilers. SIGPLAN Not. 43, 6 (2008), 183--192. Google ScholarDigital Library
- de Moura, L.M., Bjørner, N. Z3: An efficient SMT solver. In TACAS (2008), 337--340. Google ScholarDigital Library
- Feng, X., Shao, Z., Dong, Y., Guo, Y. Certifying low-level programs with hardware interrupts and preemptive threads. In PLDI (2008), 170--182. Google ScholarDigital Library
- Ford, B., Hibler, M., Lepreau, J., McGrath, R., Tullmann, P. Interface and execution models in the Fluke kernel. In OSDI (1999), 101--115. Google ScholarDigital Library
- Hawblitzel, C., Petrank, E. Automated verification of practical garbage collectors. In POPL (2009), 441--453. Google ScholarDigital Library
- Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe et al. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP) (Big Sky, MT, Oct. 2009), ACM, 207--220. Google ScholarDigital Library
- Liedtke, J., Elphinstone, K., Schönberg, S., Härtig, H., Heiser, G., Islam, N., Jaeger, T. Achieved IPC performance (still the foundation for extensibility). In Proceedings of the 6th Workshop on Hot Topics in Operating Systems (HotOS-VI) (Cape Cod, MA, May 5--6, 1997). Google ScholarDigital Library
- McCreight, A., Shao, Z., Lin, C., Li, L. A general framework for certifying garbage collectors and their mutators. In PLDI (2007), 468--479. Google ScholarDigital Library
- Morrisett, G., Walker, D., Crary, K., Glew, N. From System F to typed assembly language. In POPL '98: 25th ACM Symposium on Principles of Programming Languages (Jan. 1998), 85--97. Google ScholarDigital Library
- Turing, A. Checking a large routine. In The Early British Computer Conferences, MIT Press, Cambridge, MA, 1989, 70--72. Google ScholarDigital Library
Index Terms
- Safe to the last instruction: automated verification of a type-safe operating system
Recommendations
Safe to the last instruction: automated verification of a type-safe operating system
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and ImplementationTyped assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our ...
Safe to the last instruction: automated verification of a type-safe operating system
PLDI '10Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our ...
Automatic custom instruction identification for application-specific instruction set processors
The application-specific instruction set processors (ASIPs) have received more and more attention in recent years. ASIPs make trade-offs between flexibility and performance by extending the base instruction set of a general-purpose processor with custom ...
Comments