High-confidence operating systems

ABSTRACT

Operating systems (OSs) are among the most sophisticated software systems in widespread use, and among the most expensive and time-consuming to develop and maintain. OS software must also be robust and dependable, since OS failures can result in system crashes that corrupt user data, endanger human lives (cf. embedded systems), or provide open avenues of attack for hackers or even cyber-terrorists.

REFERENCES

• 1: Rajeev Alur , Radu Grosu , M. McDougall, Efficient Reachability Analysis of Hierarchical Reactive Machines, Proceedings of the 12th International Conference on Computer Aided Verification, p.280-295, July 15-19, 2000
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, v.36 n.5, p.203-213, May 2001
• 3: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 4: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 5: Radu Grosu , Yanhong A. Liu , Scott Smolka , Scott D. Stoller , Jingyu Yan, Automated Software Engineering Using Concurrent Class Machines, Proceedings of the 16th IEEE international conference on Automated software engineering, p.297, November 26-29, 2001
• 6: A. Kolawa and A. Hicken. Insure++: A Tool to Support Total Quality Software. http://www.parasoft.com/insure/papers/tech.htm, March 2001.
• 7: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 8: A. Tevanian and C. Minshall. File System Exerciser. http://www.codemonkey.org.uk/cruft/fsx-linux.c, 1991.