Enforcing high-level protocols in low-level software

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Enforcing high-level protocols in low-level software

Full text

Pdf (1.34 MB)

Source

Conference on Programming Language Design and Implementation archive
Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation table of contents

Snowbird, Utah, United States

Pages: 59 - 69

Year of Publication: 2001

ISBN:1-58113-414-2

Also published in ...

Authors

Robert DeLine	Microsoft Research, Microsoft Corporation, One Microsoft Way, Redmond, WA
Manuel Fähndrich	Microsoft Research, Microsoft Corporation, One Microsoft Way, Redmond, WA

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 13, Downloads (12 Months): 81, Citation Count: 118

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/378795.378811 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	T. Ball and S. Rajamani. Automatically validating temporal safety properties of software. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2001.
	2	Erik Barendsen , Sjaak Smetsers, Conventional and Uniqueness Typing in Graph Rewrite Systems, Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, p.41-51, December 15-17, 1993
	3	Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
	4	D. L. Detlefs, K. R. M. Leino, and G. Nelson. Wrestling with rep exposure. Technical Report 156, Compaq SRC, jul 1998.
	5	D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Symposium on Operating Systems Design and Implementation (OSDI 2000), Oct. 2000.
	6	Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
	7	Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
	8	David Gay , Alex Aiken, Memory management with explicit regions, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.313-323, June 17-19, 1998, Montreal, Quebec, Canada
	9	Mark P. Jones, A theory of qualified types, Science of Computer Programming, v.22 n.3, p.231-256, June 1994
	10	Mark P. Jones, Simplifying and improving qualified types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.160-169, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224198]
	11	Brian W. Kernighan , Dennis M. Ritchie, The C programming language, Prentice Hall Press, Upper Saddle River, NJ, 1989
	12	K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
	13	Conference Record of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, Jan. 1999.
	14	Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
	15	Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
	16	R. E. Strom , D. M. Yellin, Extending Typestate Checking Using Conditional Liveness Analysis, IEEE Transactions on Software Engineering, v.19 n.5, p.478-485, May 1993 [doi>10.1109/32.232013]
	17	R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
	18	Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
	19	David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
	20	David Walker , J. Gregory Morrisett, Alias Types for Recursive Data Structures, Selected papers from the Third International Workshop on Types in Compilation, p.177-206, September 21, 2000

CITED BY 118

	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
	Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, ACM SIGPLAN Notices, v.38 n.1, p.213-223, January 2003
	Naoki Kobayashi, Time regions and effects for resource usage analysis, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
	Dave Clarke , Sophia Drossopoulou, Ownership, encapsulation and the disjointness of type and effect, ACM SIGPLAN Notices, v.37 n.11, November 2002
	David Walker , Kevin Watkins, On regions and linear types (extended abstract), ACM SIGPLAN Notices, v.36 n.10, October 2001
	David Gay , Alex Aiken, Language support for regions, ACM SIGPLAN Notices, v.36 n.5, p.70-80, May 2001
	Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Sophia Drossopoulou , Ferruccio Damiani , Mariangiola Dezani-Ciancaglini , Paola Giannini, More dynamic object reclassification: Fickle∥, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.2, p.153-191, March 2002
	Dean F. Sutherland , Aaron Greenhouse , William L. Scherlis, The code of many colors: relating threads to code and shared state, ACM SIGSOFT Software Engineering Notes, v.28 n.1, January 2003
	Cormac Flanagan , Shaz Qadeer, Types for atomicity, ACM SIGPLAN Notices, v.38 n.3, March 2003
	K. Rustan M. Leino , Arnd Poetzsch-Heffter , Yunhong Zhou, Using data groups to specify and check side effects, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Sanjeev Kumar , Kai Li, Dynamic memory management for programmable devices, ACM SIGPLAN Notices, v.38 n.2 supplement, February 2003
	Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, ACM SIGPLAN Notices, v.37 n.1, p.17-32, Jan. 2002
	Aaron Greenhouse , William L. Scherlis, Assuring and evolving concurrent programs: annotations and policy, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM SIGPLAN Notices, v.37 n.1, p.331-342, Jan. 2002
	Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, ACM SIGPLAN Notices, v.37 n.5, May 2002
	G. Ramalingam , Alex Warshavsky , John Field , Deepak Goyal , Mooly Sagiv, Deriving specialized program analyses for certifying component-client conformance, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, ACM SIGPLAN Notices, v.37 n.11, November 2002
	John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006
	Dinakar Dhurjati , Sumant Kowshik , Vikram Adve , Chris Lattner, Memory safety without runtime checks or garbage collection, ACM SIGPLAN Notices, v.38 n.7, July 2003
	David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, ACM SIGOPS Operating Systems Review, v.36 n.SI, Winter 2002
	Futoshi Iwama , Naoki Kobayashi, A new type system for JVM lock primitives, Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation, p.71-82, September 12-14, 2002, Aizu, Japan
	Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Amal Ahmed , David Walker, The logical approach to stack typing, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Christopher L. Conway , Stephen A. Edwards, NDL: a domain-specific language for device drivers, ACM SIGPLAN Notices, v.39 n.7, July 2004
	Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Yichen Xie , Dawson Engler, Using redundancies to find errors, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
	Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, v.311 n.1-3, p.121-163, 23 January 2004
	Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, ACM SIGPLAN Notices, v.37 n.1, p.4-16, Jan. 2002
	Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, ACM SIGPLAN Notices, v.36 n.11, p.56-69, 11/01/2001
	Glenn Ammons , David Mandelin , Rastislav Bodík , James R. Larus, Debugging temporal specifications with concept analysis, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA
	Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Westley Weimer , George C. Necula, Finding and preventing run-time error handling mistakes, ACM SIGPLAN Notices, v.39 n.10, October 2004
	Corneliu Popeea , Wei-Ngan Chin, A type system for resource protocol verification and its correctness proof, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.135-146, August 24-25, 2004, Verona, Italy
	Patrick Lam , Viktor Kuncak , Martin Rinard, Generalized typestate checking using set interfaces and pluggable analyses, ACM SIGPLAN Notices, v.39 n.3, March 2004
	Michael Hicks , Greg Morrisett , Dan Grossman , Trevor Jim, Experience with safe manual memory-management in cyclone, Proceedings of the 4th international symposium on Memory management, October 24-25, 2004, Vancouver, BC, Canada
	Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, ACM SIGPLAN Notices, v.40 n.1, p.310-323, January 2005
	Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, ACM SIGPLAN Notices, v.37 n.5, May 2002
	John Tang Boyland , William Retert, Connecting effects and uniqueness with adoption, ACM SIGPLAN Notices, v.40 n.1, p.283-295, January 2005
	Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, ACM SIGPLAN Notices, v.40 n.1, p.98-109, January 2005
	Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Dinakar Dhurjati , Sumant Kowshik , Vikram Adve , Chris Lattner, Memory safety without garbage collection for embedded applications, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.1, p.73-111, February 2005
	V. Benjamin Livshits , Monica S. Lam, Tracking pointers with path and context sensitivity for bug detection in C programs, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
	Yichen Xie , Dawson Engler, Using redundancies to find errors, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
	Dan Grossman, Type-safe multithreading in cyclone, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Michael M. Swift , Brian N. Bershad , Henry M. Levy, Improving the reliability of commodity operating systems, ACM Transactions on Computer Systems (TOCS), v.23 n.1, p.77-110, February 2005
	Radu Rugina , Martin C. Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.185-235, March 2005
	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.264-313, March 2005
	Amal Ahmed , Matthew Fluet , Greg Morrisett, A step-indexed model of substructural state, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Kevin Bierhoff , Jonathan Aldrich, Lightweight object specification with typestates, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
	Christian Skalka, Programming Languages and Systems Security, IEEE Security and Privacy, v.3 n.3, p.80-83, May 2005
	Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, Proceedings of the 5th symposium on Operating systems design and implementation Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading , December 09-11, 2002, Boston, Massachusetts
	Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, ACM SIGPLAN Notices, v.40 n.6, June 2005
	Chris Lattner , Vikram Adve, Automatic pool allocation: improving performance by controlling data structure layout in the heap, ACM SIGPLAN Notices, v.40 n.6, June 2005
	J. Field , D. Goyal , G. Ramalingam , E. Yahav, Typestate verification: abstraction techniques and complexity results, Science of Computer Programming, v.58 n.1-2, p.57-82, October 2005
	Manuel Fähndrich , K. Rustan M. Leino, Declaring and checking non-null types in an object-oriented language, ACM SIGPLAN Notices, v.38 n.11, November 2003
	Dan Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.3, p.429-475, May 2006
	Sumant Kowshik , Dinakar Dhurjati , Vikram Adve, Ensuring code safety without runtime checks for real-time control systems, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France
	Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, ACM SIGPLAN Notices, v.38 n.9, p.213-225, September 2003
	Junfeng Yang , Ted Kremenek , Yichen Xie , Dawson Engler, MECA: an extensible, expressive system and language for statically checking security properties, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA
	Diomidis Spinellis , Panagiotis Louridas, A framework for the static verification of api calls, Journal of Systems and Software, v.80 n.7, p.1156-1168, July, 2007
	Chris Lattner , Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.75, March 20-24, 2004, Palo Alto, California
	Stephen J. Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008
	Vivek Haldar , Michael Franz, Towards trusted systems from the ground up, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC, July 01-01, 2002, Saint-Emilion, France
	Westley Weimer, Patches as better bug reports, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	Nathaniel Nystrom , Xin Qi , Andrew C. Myers, J&: nested intersection for scalable software composition, ACM SIGPLAN Notices, v.41 n.10, October 2006
	Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
	Clint Morgan , Kris De Volder , Eric Wohlstadter, A static aspect language for checking design rules, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada
	Nikhil Swamy , Michael Hicks , Greg Morrisett , Dan Grossman , Trevor Jim, Safe manual memory management in cyclone, Science of Computer Programming, v.62 n.2, p.122-144, 1 October 2006
	Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Certified In-lined Reference Monitoring on .NET, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
	David A. Naumann , Mike Barnett, Towards imperative modules: reasoning about invariants and sharing of mutable state, Theoretical Computer Science, v.365 n.1, p.143-168, 10 November 2006
	Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006
	Manuel Fähndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , Steven Levi, Language support for fast and reliable message-based communication in singularity OS, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
	Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), v.24 n.4, p.393-423, November 2006
	Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , Abdullah Ustuner, Thorough static analysis of device drivers, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
	Michael F. Spear , Tom Roeder , Orion Hodson , Galen C. Hunt , Steven Levi, Solving the starting problem: device drivers as self-describing artifacts, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
	Madanlal Musuvathi , Dawson R. Engler, Model checking large network protocol implementations, Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation, p.12-12, March 29-31, 2004, San Francisco, California
	Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.19-19, December 06-08, 2004, San Francisco, CA
	Malcolm Dowse , Andrew Butterfield, Modelling deterministic concurrent I/O, ACM SIGPLAN Notices, v.41 n.9, September 2006
	Tom Chothia , Dominic Duggan, Capability passing processes, Science of Computer Programming, v.66 n.3, p.184-204, May, 2007
	M. Pistoia , S. Chandra , S. J. Fink , E. Yahav, A survey of static analysis methods for identifying security vulnerabilities in software systems, IBM Systems Journal, v.46 n.2, p.265-288, April 2007
	Leonid Ryzhyk , Timothy Bourke , Ihor Kuz, Reliable device drivers require well-defined protocols, Proceedings of the 3rd conference on Third Workshop on Hot Topics in System Dependability, p.3-3, June 26, 2007, Edinburgh, UK
	Simon Helsen, Bisimilarity for the Region Calculus, Higher-Order and Symbolic Computation, v.17 n.4, p.347-394, December 2004
	Isil Dillig , Thomas Dillig , Eran Yahav , Satish Chandra, The CLOSER: automating resource management in java, Proceedings of the 7th international symposium on Memory management, June 07-08, 2008, Tucson, AZ, USA
	Tachio Terauchi , Alex Aiken, A capability calculus for concurrency and determinism, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.5, p.1-30, August 2008
	Xinyu Feng , Zhong Shao , Yuan Dong , Yu Guo, Certifying low-level programs with hardware interrupts and preemptive threads, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Matthew Arnold , Martin Vechev , Eran Yahav, QVM: an efficient runtime for detecting defects in deployed systems, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Xin Qi , Andrew C. Myers, Masked types for sound object initialization, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Cormac Flanagan , Stephen N. Freund , Marina Lifshin , Shaz Qadeer, Types for atomicity: Static checking and inference for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-53, July 2008
	Russ Cox , Tom Bergan , Austin T. Clements , Frans Kaashoek , Eddie Kohler, Xoc, an extension-oriented compiler for systems programming, ACM SIGOPS Operating Systems Review, v.42 n.2, March 2008
	Kevin Bierhoff , Jonathan Aldrich, Modular typestate checking of aliased objects, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Westley Weimer , George C. Necula, Exceptional situations and program reliability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.2, p.1-51, March 2008
	Christian Skalka , Scott Smith , David Van horn, Types and trace effects of higher order programs, Journal of Functional Programming, v.18 n.2, p.179-249, March 2008
	Amal Ahmed , Matthew Fluet , Greg Morrisett, L³: A Linear Language with Locations, Fundamenta Informaticae, v.77 n.4, p.397-449, December 2007
	Nomair A. Naeem , Ondrej Lhotak, Typestate-like analysis of multiple interacting objects, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Madhu Gopinathan , Sriram K. Rajamani, Enforcing object protocols by combining static and runtime analysis, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Nikhil Swamy , Michael Hicks, Verified enforcement of stateful information release policies, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, June 07-13, 2008, Tucson, AZ, USA
	Shlomi Dolev , Reuven Yagel, Self-stabilizing device drivers, ACM Transactions on Autonomous and Adaptive Systems (TAAS), v.3 n.4, p.1-29, November 2008
	Michael Roberson , Melanie Harries , Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of soundness of type systems, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Mayur Naik , Jens Palsberg, A type system equivalent to a model checker, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.5, p.1-24, August 2008
	Riccardo Pucella , Jesse A. Tov, Haskell session types with (almost) no class, Proceedings of the first ACM SIGPLAN symposium on Haskell, September 25-25, 2008, Victoria, BC, Canada
	Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: Automatically Generating Inputs of Death, ACM Transactions on Information and System Security (TISSEC), v.12 n.2, p.1-38, December 2008
	Daniel Marino , Todd Millstein, A generic type-and-effect system, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA
	Nikhil Swamy , Michael Hicks, Verified enforcement of stateful information release policies, ACM SIGPLAN Notices, v.43 n.12, December 2008
	Mariangiola Dezani-Ciancaglini , Sophia Drossopoulou , Dimitris Mostrous , Nobuko Yoshida, Objects and session types, Information and Computation, v.207 n.5, p.595-641, May, 2009
	Xinyu Feng , Zhong Shao , Yu Guo , Yuan Dong, Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads, Journal of Automated Reasoning, v.42 n.2-4, p.301-347, April 2009
	Suresh Thummalapenta , Tao Xie, Mining exception-handling rules as sequence association rules, Proceedings of the 2009 IEEE 31st International Conference on Software Engineering, p.496-506, May 16-24, 2009
	Tobias Wrigstad , Patrick Eugster , John Field , Nate Nystrom , Jan Vitek, Software hardening: a research agenda, Proceedings for the 1st workshop on Script to Program Evolution, p.58-70, July 06-06, 2009, Genova, Italy