Proof-carrying code

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Proof-carrying code

Full text

Pdf (1.17 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

Paris, France

Pages: 106 - 119

Year of Publication: 1997

ISBN:0-89791-853-3

Author

George C. Necula

School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania

Sponsors

L'Ecole des Mines de Paris : L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Ctr Natl de la Recherche Sci :
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 39, Downloads (12 Months): 222, Citation Count: 298

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/263699.263712 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	B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
	2	Robert S. Boyer , Yuan Yu, Automated proofs of object code for a widely used microprocessor, Journal of the ACM (JACM), v.43 n.1, p.166-192, Jan. 1996 [doi>10.1145/227595.227603]
	3	D. L. Clutterbuck , B. A. Carré, The verification of low-level code, Software Engineering Journal, v.3 n.3, p.97-111, May 1988
	4	FLOYD, It. W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, J. T. Schwartz, Ed. American Mathematical Society, 1967, pp. 19-32.
	5	Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
	6	MCCANNE, S., AND JACOBSON, V. The BSD packet filter: A new architecture for user-level packet capture. In The Winter 1993 USENIX Con- .terence (Jan. 1993), USENIX Association, pp. 259- 269.
	7	MILLER, D., NADATHUR, G., PFENNING, F., AND SCEDROV, A. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51 (1991), 125-157.
	8	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	9	J. Mogul , R. Rashid , M. Accetta, The packer filter: an efficient mechanism for user-level network code, Proceedings of the eleventh ACM Symposium on Operating systems principles, p.39-51, November 08-11, 1987, Austin, Texas, United States
	10	NECULA, G. C., AND LEE, P. Proof-carrying code. Technical Report CMU-CS-96-165, Computer Science Department, Carnegie Mellon University, Sept. 1996. Also appeared as FOX memorandum CMU-CS-FOX-96-03.
	11	George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
	12	F. Pfening, Elf: a language for logic definition and verified metaprogramming, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.313-322, June 1989, Pacific Grove, California, United States
	13	François Rouaix, A Web navigator with applets in Caml, Proceedings of the fifth international World Wide Web conference on Computer networks and ISDN systems, p.1365-1371, May 1996, Paris, France
	14	Richard L. Sites, Alpha architecture reference manual, Digital Press, Newton, MA, 1992
	15	D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
	16	Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States

CITED BY 298

	Dennis Brylow , Niels Damgaard , Jens Palsberg, Static checking of interrupt-driven software, Proceedings of the 23rd International Conference on Software Engineering, p.47-56, May 12-19, 2001, Toronto, Ontario, Canada
	Stefan Monnier , Bratin Saha , Zhong Shao, Principled scavenging, ACM SIGPLAN Notices, v.36 n.5, p.81-91, May 2001
	David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA
	Philip W. L. Fong , Robert D. Cameron, Proof linking: an architecture for modular verification of dynamically-linked mobile code, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.222-230, Nov. 1998
	Andrew W. Appel , Edward W. Felten, Proof-carrying authentication, Proceedings of the 6th ACM conference on Computer and communications security, p.52-62, November 01-04, 1999, Kent Ridge Digital Labs, Singapore
	Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA
	Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, ACM SIGPLAN Notices, v.36 n.3, p.14-26, March 2001
	Andrew D. Gordon , Don Syme, Typing a multi-language intermediate code, ACM SIGPLAN Notices, v.36 n.3, p.248-260, March 2001
	Andrew W. Appel , Amy P. Felty, A semantic model of types and machine instructions for proof-carrying code, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.243-253, January 19-21, 2000, Boston, MA, USA
	Christopher A. Stone , Robert Harper, Deciding type equivalence in a language with singleton kinds, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 19-21, 2000, Boston, MA, USA
	Emin Gün Sirer , Brian N. Bershad, Using production grammars in software testing, ACM SIGPLAN Notices, v.35 n.1, p.1-13, Jan. 2000
	Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Untrusted hosts and confidentiality: secure program partitioning, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
	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
	Ramesh Jagannathan , Paolo A.G. Sivilotti, Increasing client-side confidence in remote component implementations, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
	Sung-Soo Lim , Kihwal Lee , Lui Sha, Ensuring integrity and service availability in a web-based control laboratory, Real-time system security, Nova Science Publishers, Inc., Commack, NY, 2003
	Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA
	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999
	Philip W. L. Fong , Robert D. Cameron, Proof linking: modular verification of mobile programs in the presence of lazy, dynamic linking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.379-409, Oct. 2000
	Michael Godfrey , Tobias Mayr , Praveen Seshadri , Thorsten von Eicken, Secure and portable database extensibility, ACM SIGMOD Record, v.27 n.2, p.390-401, June 1998
	Daniel C. Wang , Andrew W. Appel, Type-preserving garbage collectors, ACM SIGPLAN Notices, v.36 n.3, p.166-178, March 2001
	R. Sekar , C. R. Ramakrishnan , I. V. Ramakrishnan , S. A. Smolka, Model-Carrying Code (MCC): a new paradigm for mobile-code security, Proceedings of the 2001 workshop on New security paradigms, September 10-13, 2001, Cloudcroft, New Mexico
	Mauricio Serrano , Rajesh Bordawekar , Sam Midkiff , Manish Gupta, Quicksilver: a quasi-static compiler for Java, ACM SIGPLAN Notices, v.35 n.10, p.66-82, Oct. 2000
	Nael B. Abu-Ghazaleh , Dhananjay S. Phatak, Verification caching: towards efficient and secure mobile code execution environments, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
	Sorin Lerner , Todd Millstein , Craig Chambers, Automatically proving the correctness of compiler optimizations, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Stephen N. Freund , John C. Mitchell, A formal framework for the Java bytecode language and verifier, ACM SIGPLAN Notices, v.34 n.10, p.147-166, Oct. 1999
	Christopher League , Zhong Shao , Valery Trifonov, Type-preserving compilation of Featherweight Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.2, p.112-152, March 2002
	Xavier Leroy , François Rouaix, Security properties of typed applets, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.391-403, January 19-21, 1998, San Diego, California, United States
	David Lacey , Neil D. Jones , Eric Van Wyk , Carl Christian Frederiksen, Proving correctness of compiler optimizations by temporal logic, ACM SIGPLAN Notices, v.37 n.1, p.283-294, Jan. 2002
	Grzegorz Czajkowski , Thorsten von Eicken, JRes: a resource accounting interface for Java, ACM SIGPLAN Notices, v.33 n.10, p.21-35, Oct. 1998
	George C. Necula , Peter Lee, The design and implementation of a certifying compiler, ACM SIGPLAN Notices, v.33 n.5, p.333-344, May 1998
	Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999
	Zhong Shao , Christopher League , Stefan Monnier, Implementing typed intermediate languages, ACM SIGPLAN Notices, v.34 n.1, p.313-323, Jan. 1999
	Michael Hicks , Jonathan T. Moore , Scott Nettles, Dynamic software updating, ACM SIGPLAN Notices, v.36 n.5, p.13-23, May 2001
	Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, ACM SIGPLAN Notices, v.35 n.5, p.95-107, May 2000
	Michele Bugliesi , Giuseppe Castagna, Secure safe ambients, ACM SIGPLAN Notices, v.36 n.3, p.222-235, March 2001
	James Riely , Matthew Hennessy, Trust and partial typing in open systems of mobile agents, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-104, January 20-22, 1999, San Antonio, Texas, United States
	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
	Nobuko Yoshida , Matthew Hennessy, Assigning types to processes, Information and Computation, v.174 n.2, p.143-179, May 1 2002
	George C. Necula , S. P. Rahul, Oracle-based checking of untrusted software, ACM SIGPLAN Notices, v.36 n.3, p.142-154, March 2001
	Michael Hicks , Pankaj Kakkar , Jonathan T. Moore , Carl A. Gunter , Scott Nettles, PLAN: a packet language for active networks, ACM SIGPLAN Notices, v.34 n.1, p.86-93, Jan. 1999
	Zhong Shao , Bratin Saha , Valery Trifonov , Nikolaos Papaspyrou, A type system for certified binaries, ACM SIGPLAN Notices, v.37 n.1, p.217-232, Jan. 2002
	Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Secure program partitioning, ACM Transactions on Computer Systems (TOCS), v.20 n.3, p.283-328, August 2002
	Craig Partridge , Alex C. Snoeren , W. Timothy Strayer , Beverly Schwartz , Matthew Condell , Isidro Castiñeyra, FIRE: flexible Intra-AS routing environment, ACM SIGCOMM Computer Communication Review, v.30 n.4, p.191-203, October 2000
	Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000
	Andrew C. Myers , Barbara Liskov, A decentralized model for information flow control, ACM SIGOPS Operating Systems Review, v.31 n.5, p.129-142, Dec. 1997
	Zhichen Xu , Barton P. Miller , Thomas Reps, Safety checking of machine code, ACM SIGPLAN Notices, v.35 n.5, p.70-82, May 2000
	Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States
	Premkumar T. Devanbu , Stuart Stubblebine, Software engineering for security: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.227-239, June 04-11, 2000, Limerick, Ireland
	Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Computability classes for enforcement mechanisms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.175-205, January 2006
	Premkumar T. Devanbu , Philip W-L Fong , Stuart G. Stubblebine, Techniques for trusted software engineering, Proceedings of the 20th international conference on Software engineering, p.126-135, April 19-25, 1998, Kyoto, Japan
	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States
	Gilles Grimaud , Jean-Louis Lanet , Jean-Jacques Vandewalle, FACADE: a typed intermediate language dedicated to smart cards, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.476-493, Nov. 1999
	Xavier Leroy, Bytecode verification on Java smart cards, Software—Practice & Experience, v.32 n.4, p.319-340, 10 April 2002
	Robert van Engelen , David Whalley , Xin Yuan, Validation of code-improving transformations for embeded systems, Proceedings of the 2003 ACM symposium on Applied computing, March 09-12, 2003, Melbourne, Florida
	Christopher Colby , Karl Crary , Robert Harper , Peter Lee , Frank Pfenning, Automated techniques for provably safe mobile code, Theoretical Computer Science, v.290 n.2, p.1175-1199, 2 January 2003
	Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada
	Benjamin C. Pierce, Type systems, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
	Neal Glew , Greg Morrisett, Type-safe linking and modular assembly language, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 20-22, 1999, San Antonio, Texas, United States
	Juan Chen , Dinghao Wu , Andrew W. Appel , Hai Fang, A provably sound TAL for back-end optimization, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Oliver Spatscheck , Larry L. Peterson, Defending against denial of service attacks in Scout, Proceedings of the third symposium on Operating systems design and implementation, p.59-72, February 1999, New Orleans, Louisiana, United States
	Cindy Kong , P. Alexander , Darryl Dieckman, Formal modeling of active network nodes using PVS, Proceedings of the third workshop on Formal methods in software practice, p.49-59, August 2000, Portland, Oregon, United States
	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
	George C. Necula, Proof-carrying code (abstract): design, implementation and applications, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.175-177, September 20-23, 2000, Montreal, Quebec, Canada
	An Approach for Secure Software Installation, Proceedings of the 16th USENIX conference on System administration, November 03-08, 2002, Philadelphia, PA
	Wolfram Amme , Niall Dalton , Jeffery von Ronne , Michael Franz, SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form, ACM SIGPLAN Notices, v.36 n.5, p.137-147, May 2001
	John Zachary , Richard Brooks, Bidirectional mobile code trust management using tamper resistant hardware, Mobile Networks and Applications, v.8 n.2, p.137-143, April 2003
	Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, ACM SIGPLAN Notices, v.38 n.1, p.185-197, January 2003
	G. Denys , F. Piessens , F. Matthijs, A survey of customizability in operating systems research, ACM Computing Surveys (CSUR), v.34 n.4, p.450-468, December 2002
	Jeffery von Ronne , Andreas Hartmann , Wolfram Amme , Michael Franz, Efficient online optimization by utilizing offline analysis and the safeTSA representation, Proceedings of the inaugural conference on the Principles and Practice of programming, 2002 and Proceedings of the second workshop on Intermediate representation engineering for virtual machines, 2002, June 13-14, 2002, Dublin, Ireland
	Gary McGraw , Greg Morrisett, Attacking Malicious Code: A Report to the Infosec Research Council, IEEE Software, v.17 n.5, p.33-41, September 2000
	Amal Ahmed , David Walker, The logical approach to stack typing, ACM SIGPLAN Notices, v.38 n.3, March 2003
	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
	Hayo Thielecke, Frame rules from answer types for code pointers, ACM SIGPLAN Notices, v.41 n.1, p.309-319, January 2006
	Michael J. Lewis , Adam J. Ferrari , Marty A. Humphrey , John F. Karpovich , Mark M. Morgan , Anand Natrajan , Anh Nguyen-Tuong , Glenn S. Wasson , Andrew S. Grimshaw, Support for extensibility and site autonomy in the Legion grid system object model, Journal of Parallel and Distributed Computing, v.63 n.5, p.525-538, May 2003
	Vivek Haldar , Christian H. Stork , Michael Franz, The source is the proof, Proceedings of the 2002 workshop on New security paradigms, September 23-26, 2002, Virginia Beach, Virginia
	Sergio Loureiro , Refik Molva , Alain Pannetrat, Secure Data Collection with Updates, Electronic Commerce Research, v.1 n.1-2, p.119-130, February/March 2001
	Sumit Gulwani , George C. Necula, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols, Information and Computation, v.199 n.1-2, p.107-131, 25 May 2005
	Hongwei Xi , Songtao Xia, Towards array bound check elimination in Java ^TM virtual machine language, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.14, November 08-11, 1999, Mississauga, Ontario, Canada
	Premkumar Devanbu , Michael Gertz , Charles Martel , Stuart G. Stubblebine, Authentic data publication over the internet, Journal of Computer Security, v.11 n.3, p.291-314, 1 March 2003
	Dinghao Wu , Andrew W. Appel , Aaron Stump, Foundational proof checkers with small witnesses, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.264-274, August 27-29, 2003, Uppsala, Sweden
	Parveen Patel, An introduction to active network node operating systems, Crossroads, v.9 n.2, p.21-26, December 2002
	Xavier Rival, Symbolic transfer function-based approaches to certified compilation, ACM SIGPLAN Notices, v.39 n.1, p.1-13, January 2004
	Paul Barham , Boris Dragovic , Keir Fraser , Steven Hand , Tim Harris , Alex Ho , Rolf Neugebauer , Ian Pratt , Andrew Warfield, Xen and the art of virtualization, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
	Dave Clarke , Michael Richmond , James Noble, Saving the world from bad beans: deployment-time confinement checking, ACM SIGPLAN Notices, v.38 n.11, November 2003
	Michael Franz , Deepak Chandra , Andreas Gal , Vivek Haldar , Fermín Reig , Ning Wang, A portable Virtual Machine target for Proof-Carrying Code, Proceedings of the 2003 workshop on Interpreters, virtual machines and emulators, p.24-31, June 12-12, 2003, San Diego, California
	R. Sekar , V.N. Venkatakrishnan , Samik Basu , Sandeep Bhatkar , Daniel C. DuVarney, Model-carrying code: a practical approach for safe execution of untrusted applications, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
	Andrew D. Gordon , Alan Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, v.11 n.4, p.451-519, 01/01/2004
	Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, ACM SIGPLAN Notices, v.39 n.1, p.232-244, January 2004
	Daniele Gorla , Rosario Pugliese, Controlling data movement in global computing applications, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus
	Daniel C. DuVarney , V. N. Venkatakrishnan , Sandeep Bhatkar, SELF: a transparent security extension for ELF binaries, Proceedings of the 2003 workshop on New security paradigms, August 18-21, 2003, Ascona, Switzerland
	Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005
	Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001
	Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, ACM SIGPLAN Notices, v.33 n.5, p.249-257, May 1998
	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
	Andrew C. Myers , Barbara Liskov, Protecting privacy using the decentralized label model, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.410-442, Oct. 2000
	Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, ACM SIGPLAN Notices, v.41 n.1, p.42-54, January 2006
	P. Inverardi , F. Mancinelli , G. Marinelli, Correct deployment and adaptation of software applications on heterogenous (mobile) devices, Proceedings of the first workshop on Self-healing systems, November 18-19, 2002, Charleston, South Carolina
	Xavier Leroy, Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning, v.30 n.3-4, p.235-269, 2003
	Emmett Witchel , Josh Cates , Krste Asanović, Mondrian memory protection, ACM SIGPLAN Notices, v.37 n.10, October 2002
	Philip W. L. Fong, Pluggable verification modules: an extensible protection mechanism for the JVM, ACM SIGPLAN Notices, v.39 n.10, October 2004
	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
	Michael Franz, The Java Virtual Machine: A Passing Fad?, IEEE Software, v.15 n.6, p.26-29, November 1998
	David Tarditi , Greg Morrisett , Perry Cheng , Chris Stone , Robert Harper , Peter Lee, TIL: a type-directed, optimizing compiler for ML, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Dachuan Yu , Nadeem A. Hamid , Zhong Shao, Building certified libraries for PCC: dynamic storage allocation, Science of Computer Programming, v.50 n.1-3, p.101-127, March 2004
	Stefan Pleisch , André Schiper, Approaches to fault-tolerant and transactional mobile agent execution---an algorithmic view, ACM Computing Surveys (CSUR), v.36 n.3, p.219-262, September 2004
	Sorin Lerner , Todd Millstein , Erika Rice , Craig Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, ACM SIGPLAN Notices, v.40 n.1, p.364-377, January 2005
	Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Dahlia Malkhi , Michael K. Reiter, Secure Execution of Java Applets Using a Remote Playground, IEEE Transactions on Software Engineering, v.26 n.12, p.1197-1209, December 2000
	Licia Capra, Engineering human trust in mobile system collaborations, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Michael F. Ringenburg , Dan Grossman, Types for describing coordinated data structures, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.25-36, January 10-10, 2005, Long Beach, California, USA
	Robert van Engelen , David Whalley , Xin Yuan, Automatic validation of code-improving transformations on low-level program representations, Science of Computer Programming, v.52 n.1-3, p.257-280, August 2004
	Joseph C. Vanderwaart , Karl Crary, Automated and certified conformance to responsiveness policies, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.79-90, January 10-10, 2005, Long Beach, California, USA
	Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, Type-based verification of sssembly language for compiler debugging, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.91-102, January 10-10, 2005, Long Beach, California, USA
	Chandra Krintz, Using adaptive optimization techniques to teach mobile Java computing, Proceedings of the inaugural conference on the Principles and Practice of programming, 2002 and Proceedings of the second workshop on Intermediate representation engineering for virtual machines, 2002, June 13-14, 2002, Dublin, Ireland
	Darko Kirovski , Milenko Drinić , Miodrag Potkonjak, Enabling trusted software integrity, ACM SIGPLAN Notices, v.37 n.10, October 2002
	P. T. Devanbu , S. G. Stubblebine, Stack and Queue Integrity on Hostile Platforms, IEEE Transactions on Software Engineering, v.28 n.1, p.100-108, January 2002
	Hongwei Xi , Robert Harper, A dependently typed assembly language, ACM SIGPLAN Notices, v.36 n.10, October 2001
	Joseph C. Vanderwaart , Karl Crary, A typed interface for garbage collection, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Atsushi Ohori, Register allocation by proof transformation, Science of Computer Programming, v.50 n.1-3, p.161-187, March 2004
	Lars Birkedal , Noah Torp-Smith , John C. Reynolds, Local reasoning about a copying garbage collector, ACM SIGPLAN Notices, v.39 n.1, p.220-231, January 2004
	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
	Zhaozhong Ni , Zhong Shao, Certified assembly programming with embedded code pointers, ACM SIGPLAN Notices, v.41 n.1, p.320-333, January 2006
	Ahmad-Reza Sadeghi , Christian Stüble, Property-based attestation for computing platforms: caring about properties, not mechanisms, Proceedings of the 2004 workshop on New security paradigms, September 20-23, 2004, Nova Scotia, Canada
	Mike Jochen , Anteneh Addis Anteneh , Lori L. Pollock , Lisa M. Marvel, Enabling control over adaptive program transformation for dynamically evolving mobile software validation, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	Christian Lindig, Random testing of C calling conventions, Proceedings of the sixth international symposium on Automated analysis-driven debugging, p.3-12, September 19-21, 2005, Monterey, California, USA
	Bart De Win , Frank Piessens , Jan Smans , Wouter Joosen, Towards a unifying view on security contracts, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	Manuel V. Hermenegildo , Elvira Albert , Pedro López-García , Germán Puebla, Abstraction carrying code and resource-awareness, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.1-11, July 11-13, 2005, Lisbon, Portugal
	Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, ACM SIGPLAN Notices, v.40 n.6, June 2005
	Claude Kirchner , Pierre-Etienne Moreau , Antoine Reilles, Formal validation of pattern matching code, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.187-197, July 11-13, 2005, Lisbon, Portugal
	Vijay S. Menon , Neal Glew , Brian R. Murphy , Andrew McCreight , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Leaf Petersen, A verifiable SSA program representation for aggressive compiler optimization, ACM SIGPLAN Notices, v.41 n.1, p.397-408, January 2006
	Michael Hicks , Scott Nettles, Dynamic software updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1049-1096, November 2005
	Martín Abadi , Mihai Budiu , Úlfar Erlingsson , Jay Ligatti, Control-flow integrity, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA
	Benjamin A. Kuperman , Carla E. Brodley , Hilmi Ozdoganoglu , T. N. Vijaykumar , Ankit Jalote, Detection and prevention of stack buffer overflow attacks, Communications of the ACM, v.48 n.11, p.50-56, November 2005
	Cormac Flanagan, Hybrid type checking, ACM SIGPLAN Notices, v.41 n.1, p.245-256, January 2006
	Orna Kupferman , Moshe Y. Vardi, From complementation to certification, Theoretical Computer Science, v.345 n.1, p.83-100, 21 November 2005
	Guangyu Chen , Mahmut Kandemir, Verifiable annotations for embedded java environments, Proceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems, September 24-27, 2005, San Francisco, California, USA
	George C. Necula , Peter Lee, The design and implementation of a certifying compiler, ACM SIGPLAN Notices, v.39 n.4, April 2004
	George C. Necula , Peter Lee, The design and implementation of a certifying compiler, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Joseph Zambreno , Alok Choudhary , Rahul Simha , Bhagi Narahari , Nasir Memon, SAFE-OPS: An approach to embedded software security, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.1, p.189-210, February 2005
	Juan Chen , David Tarditi, A simple typed intermediate language for object-oriented languages, ACM SIGPLAN Notices, v.40 n.1, p.38-49, January 2005
	Kim B. Bruce , Robert L. Scot Drysdale , Charles Kelemen , Allen Tucker, Why math?, Communications of the ACM, v.46 n.9, September 2003
	Subhashini Raghunathan , Armin R. Mikler , Cliff Cozzolino, Secure agent computation: X.509 proxy certificates in a multi-lingual agent framework, Journal of Systems and Software, v.75 n.1-2, p.125-137, 15 February 2005
	Frank Pfenning, Logical frameworks, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Xinyu Feng , Zhong Shao, Modular verification of concurrent assembly code with dynamic thread creation and termination, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Todd L. Veldhuizen, Tradeoffs in metaprogramming, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Scott A. Thibault , Renaud Marlet , Charles Consel, Domain-Specific Languages: From Design to Implementation Application to Video Device Drivers Generation, IEEE Transactions on Software Engineering, v.25 n.3, p.363-377, May 1999
	Fabio Mancinelli , Paola Inverardi, A resource model for adaptable applications, Proceedings of the 2006 international workshop on Self-adaptation and self-managing systems, May 21-22, 2006, Shanghai, China
	Lenore Zuck , Amir Pnueli , Benjamin Goldberg , Clark Barrett , Yi Fang , Ying Hu, Translation and Run-Time Validation of Loop Transformations, Formal Methods in System Design, v.27 n.3, p.335-360, November 2005
	Amit Vasudevan , Ramesh Yerraballi , Ashish Chawla, A high performance Kernel-Less Operating System architecture, Proceedings of the Twenty-eighth Australasian conference on Computer Science, p.287-296, January 01, 2005, Newcastle, Australia
	Roshan G. Ragel , Sri Parameswaran, IMPRES: integrated monitoring for processor reliability and security, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Ludovic Casset , Jean-Louis Lanet, Increasing smart card dependability, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC, July 01-01, 2002, Saint-Emilion, France
	Hassan Artail , Elie Kahale, MAWS: a platform-independent framework for mobile agents using web services, Journal of Parallel and Distributed Computing, v.66 n.3, p.428-443, March 2006
	D. R. Ghica , A. S. Murawski , C.-H. L. Ong, Syntactic control of concurrency, Theoretical Computer Science, v.350 n.2, p.234-251, 7 February 2006
	Olga Gelbart , Bhagirath Narahari , Rahul Simha, SPEE: a secure program execution environment tool using code integrity checking, Journal of High Speed Networks, v.15 n.1, p.21-32, January 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
	P. Pepper , M. Cebulla , K. Didrich , W. Grieskamp, From program languages to software languages, Journal of Systems and Software, v.60 n.2, p.91-101, 1 February 2002
	Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, ACM SIGPLAN Notices, v.38 n.9, p.213-225, September 2003
	Hongwei Xi, Dependent Types for Program Termination Verification, Higher-Order and Symbolic Computation, v.15 n.1, p.91-131, March 2002
	Úlfar Erlingsson , John MacCormick, Ad hoc extensibility and access control, ACM SIGOPS Operating Systems Review, v.40 n.3, July 2006
	Gerwin Klein , Ralf Huuck, High assurance system software, Proceedings of the 10th Australian workshop on Safety critical systems and software, p.59-67, August 25, 2005, Sydney, Australia
	Pablo Garralda , Eduardo Bonelli , Adriana Compagnoni , Mariangiola Dezani-Ciancaglini, Boxed ambients with communication interfaces, Mathematical Structures in Computer Science, v.17 n.4, p.587-645, August 2007
	Dominic Duggan, Type-based cryptographic operations, Journal of Computer Security, v.12 n.3,4, p.485-550, May 2004
	Michael Zeller , Aaron Stump , Morgan Deters, Signature Compilation for the Edinburgh Logical Framework, Electronic Notes in Theoretical Computer Science (ENTCS), 196, p.129-135, January, 2008
	Lieven Desmet , Wouter Joosen , Fabio Massacci , Katsiaryna Naliuka , Pieter Philippaerts , Frank Piessens , Dries Vanoverberghe, A flexible security architecture to support third-party applications on mobile devices, Proceedings of the 2007 ACM workshop on Computer security architecture, November 02-02, 2007, Fairfax, Virginia, USA
	Jan Olaf Blech , Arnd Poetzsch-Heffter, A Certifying Code Generation Phase, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.4, p.65-82, November, 2007
	Noah Torp-Smith , Lars Birkedal , John C. Reynolds, Local reasoning about a copying garbage collector, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-58, July 2008
	Milenko Drinic , Darko Kirovski, A Hardware-Software Platform for Intrusion Prevention, Proceedings of the 37th annual IEEE/ACM International Symposium on Microarchitecture, p.233-242, December 04-08, 2004, Portland, Oregon
	Neil Vachharajani , Matthew J. Bridges , Jonathan Chang , Ram Rangan , Guilherme Ottoni , Jason A. Blome , George A. Reis , Manish Vachharajani , David I. August, RIFLE: An Architectural Framework for User-Centric Information-Flow Security, Proceedings of the 37th annual IEEE/ACM International Symposium on Microarchitecture, p.243-254, December 04-08, 2004, Portland, Oregon
	C. Bernardeschi , N. De Francesco , G. Lettieri , L. Martini , P. Masci, Decomposing bytecode verification by abstract interpretation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.1, p.1-63, December 2008
	Nadeem A. Hamid , Zhong Shao , Valery Trifonov , Stefan Monnier , Zhaozhong Ni, A Syntactic Approach to Foundational Proof-Carrying Code, Journal of Automated Reasoning, v.31 n.3-4, p.191-229, 2003
	Andrew W. Appel , Neophytos Michael , Aaron Stump , Roberto Virga, A Trustworthy Proof Checker, Journal of Automated Reasoning, v.31 n.3-4, p.231-260, 2003
	Eva Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, v.31 n.3-4, p.303-334, 2003
	James Riely , Matthew Hennessy, Trust and Partial Typing in Open Systems of Mobile Agents, Journal of Automated Reasoning, v.31 n.3-4, p.335-370, 2003
	Jeff Polakow , Christian Skalka, Specifying distributed trust management in LolliMon, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
	Martin Naedele , Thomas E. Koch, Trust and tamper-proof software delivery, Proceedings of the 2006 international workshop on Software engineering for secure systems, May 20-21, 2006, Shanghai, China
	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
	Pieter H. Hartel , Luc Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys (CSUR), v.33 n.4, p.517-558, December 2001
	Cristiano Calcagno, Stratified operational semantics for safety and correctness of the region calculus, ACM SIGPLAN Notices, v.36 n.3, p.155-165, March 2001
	Gary T. Leavens , Jean-Raymond Abrial , Don Batory , Michael Butler , Alessandro Coglio , Kathi Fisler , Eric Hehner , Cliff Jones , Dale Miller , Simon Peyton-Jones , Murali Sitaraman , Douglas R. Smith , Aaron Stump, Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	Nadeem Abdul Hamid, Certified memory management for proof-carrying code: a region-based type system and runtime library, Proceedings of the 43rd annual southeast regional conference, March 18-20, 2005, Kennesaw, Georgia
	Zhong Shao, Typed common intermediate format, Proceedings of the Conference on Domain-Specific Languages on Conference on Domain-Specific Languages (DSL), 1997, p.8-8, October 15-17, 1997, Santa Barbara, California
	Chris Hawblitzel , Chi-Chao Chang , Grzegorz Czajkowski , Deyu Hu , Thorsten von Eicken, Implementing multiple protection domains in java, Proceedings of the Annual Technical Conference on USENIX Annual Technical Conference, 1998, p.22-22, June 15-19, 1998, New Orleans, Louisiana
	Scott Thibault , Renaud Marlet , Charles Consel, A domain specific language for video device drivers: from design to implementation, Proceedings of the Conference on Domain-Specific Languages on Conference on Domain-Specific Languages (DSL), 1997, p.2-2, October 15-17, 1997, Santa Barbara, California
	Emin Gün Sirer , Brian N. Bershad, Using production grammars in software testing, Proceedings of the 2nd conference on Conference on Domain-Specific Languages, p.1-1, October 03-05, 1999, Austin, Texas
	Austin Donnelly, Lightweight thread tunnelling in network applications, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.50 n.14, p.2462-2474, 5 October 2006
	Roberto M. Amadio , Silvano Dal Zilio, Resource control for synchronous cooperative threads, Theoretical Computer Science, v.358 n.2, p.229-254, 7 August 2006
	Ewen Denney , Bernd Fischer, A generic annotation inference algorithm for the safety certification of automatically generated code, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	Michael Franz , Deepak Chandra , Andreas Gal , Vivek Haldar , Christian W. Probst , Fermín Reig , Ning Wang, A portable virtual machine target for proof-carrying code, Science of Computer Programming, v.57 n.3, p.275-294, September 2005
	Michael Hohmuth , Hendrik Tews , Shane G. Stephens, Applying source-code verification to a microkernel: the VFiasco project, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC, July 01-01, 2002, Saint-Emilion, France
	Damiano Zanardini, Abstract non-interference in a fragment of Java bytecode, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
	Yutaka Matsuno , Atsushi Ohori, A type system equivalent to static single assignment, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
	Frédéric Besson , Thomas Jensen , David Pichardie, Proof-carrying code from certified abstract interpretation and fixpoint compression, Theoretical Computer Science, v.364 n.3, p.273-291, 8 November 2006
	Peeter Laud , Tarmo Uustalu , Varmo Vene, Type systems equivalent to data-flow analyses for imperative languages, Theoretical Computer Science, v.364 n.3, p.292-310, 8 November 2006
	Gilles Barthe , Tamara Rezk , Amitabh Basu, Security types preserving compilation, Computer Languages, Systems and Structures, v.33 n.2, p.35-59, July, 2007
	Rocco De Nicola , Daniele Gorla , Rosario Pugliese, Confining data and processes in global computing applications, Science of Computer Programming, v.63 n.1, p.57-87, November 2006
	Jeffrey C. Mogul , Martin Arlitt, SC2D: an alternative to trace anonymization, Proceedings of the 2006 SIGCOMM workshop on Mining network data, p.323-328, September 11-15, 2006, Pisa, Italy
	Sonia Fagorzi , Elena Zucca, A Calculus of Components with Dynamic Type-Checking, Electronic Notes in Theoretical Computer Science (ENTCS), 182, p.73-90, June, 2007
	Fabio Mancinelli , Paola Inverardi, Quantitative resource-oriented analysis of Java (Adaptable) applications, Proceedings of the 6th international workshop on Software and performance, February 05-08, 2007, Buenes Aires, Argentina
	Fabio Mancinelli , Paola Inverardi, Quantitative resource-oriented analysis of Java (Adaptable) applications, Proceedings of the 6th international workshop on Software and performance, February 05-08, 2007, Buenes Aires, Argentina
	Surasak Sanguanpong , Urupoj Kanlayasiri, Worm damage minimization in enterprise networks, International Journal of Human-Computer Studies, v.65 n.1, p.3-16, January, 2007
	Irem Aktug , Katsiaryna Naliuka, ConSpec -- A Formal Language for Policy Specification, Electronic Notes in Theoretical Computer Science (ENTCS), v.197 n.1, p.45-58, February, 2008
	Umesh Shankar , Monica Chew , J. D. Tygar, Side effects are not sufficient to authenticate software, Proceedings of the 13th conference on USENIX Security Symposium, p.7-7, August 09-13, 2004, San Diego, CA
	Damien Deville , Gilles Grimaud, Building an "impossible" verifier on a java card, Proceedings of the 2nd conference on Industrial Experiences with Systems Software, p.2-2, December 08, 2002, Boston, MA
	David Larochelle , David Evans, Statically detecting likely buffer overflow vulnerabilities, Proceedings of the 10th conference on USENIX Security Symposium, p.14-14, August 13-17, 2001, Washington, D.C.
	Drew Dean , Alan J. Hu, Fixing races for fun and profit: how to use access(2), Proceedings of the 13th conference on USENIX Security Symposium, p.14-14, August 09-13, 2004, San Diego, CA
	Sunil Soman , Chandra Krintz , Giovanni Vigna, Detecting malicious java code using virtual machine auditing, Proceedings of the 12th conference on USENIX Security Symposium, p.11-11, August 04-08, 2003, Washington, DC
	Franco Barbanera , Michele Bugliesi , Mariangiola Dezani-Ciancaglini , Vladimiro Sassone, Space-aware ambients and processes, Theoretical Computer Science, v.373 n.1-2, p.41-69, March, 2007
	Chien-Liang Fok , Gruia-Catalin Roman , Chenyang Lu, Agilla: A mobile agent middleware for self-adaptive wireless sensor networks, ACM Transactions on Autonomous and Adaptive Systems (TAAS), v.4 n.3, p.1-26, July 2009
	Nick Benton , Uri Zarfaty, Formalizing and verifying semantic type soundness of a simple compiler, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
	Ivan Ganev , Greg Eisenhauer , Karsten Schwan, Kernel plugins: when a VM is too much, Proceedings of the 3rd conference on Virtual Machine Research And Technology Symposium, p.7-7, May 06-07, 2004, San Jose, California
	Sanna Tuohimaa , Ville Leppänen, A compact aspect-based security monitor for J2ME applications, Proceedings of the 2007 international conference on Computer systems and technologies, June 14-15, 2007, Bulgaria
	Nimisha V. Mehta , Karen R. Sollins, Expanding and extending the security features of java, Proceedings of the 7th conference on USENIX Security Symposium, 1998, p.12-12, January 26-29, 1998, San Antonio, Texas
	Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, ACM SIGPLAN Notices, v.41 n.9, September 2006
	Adam Chlipala, Modular development of certified program verifiers with a proof assistant, ACM SIGPLAN Notices, v.41 n.9, September 2006
	David Walker , Lester Mackey , Jay Ligatti , George A. Reis , David I. August, Static typing for a faulty lambda calculus, ACM SIGPLAN Notices, v.41 n.9, September 2006
	David Larochelle , David Evans, Statically detecting likely buffer overflow vulnerabilities, Proceedings of the 10th conference on USENIX Security Symposium, p.14-14, August 13-17, 2001, Washington, D.C.
	Tom Chothia , Dominic Duggan , Ye Wu, An End-To-End Approach to Distributed Policy Language Implementation, Electronic Notes in Theoretical Computer Science (ENTCS), v.171 n.4, p.3-21, July, 2007
	Oleg Kiselyov , Chung-chieh Shan, Lightweight Static Capabilities, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.79-104, June, 2007
	Gilles Barthe , César Kunz, Certificate translation for specification-preserving advices, Proceedings of the 7th workshop on Foundations of aspect-oriented languages, p.9-18, April 01-01, 2008, Brussels, Belgium
	Karl Crary , Susmit Sarkar, Foundational certified code in the Twelf metalogical framework, ACM Transactions on Computational Logic (TOCL), v.9 n.3, p.1-26, June 2008
	Manuel Montenegro , Ricardo Peña , Clara Segura, A type system for safe memory management and its proof of correctness, Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, July 15-17, 2008, Valencia, Spain
	Avik Chaudhuri , Prasad Naldurg , Sriram Rajamani, A type system for data-flow integrity on windows vista, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, June 07-13, 2008, Tucson, AZ, USA
	Tom In der Rieden , Alexandra Tsyban, CVM -- A Verified Framework for Microkernel Programmers, Electronic Notes in Theoretical Computer Science (ENTCS), 217, p.151-168, July, 2008
	Nadeem Abdul Hamid, Integrating a certified memory management runtime with proof-carrying code, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
	Song Fu , Cheng-Zhong Xu, Coordinated access control with temporal and spatial constraints on mobile execution in coalition environments, Future Generation Computer Systems, v.23 n.6, p.804-815, July, 2007
	Ram Kumar , Eddie Kohler , Mani Srivastava, Harbor: software-based memory protection for sensor nodes, Proceedings of the 6th international conference on Information processing in sensor networks, April 25-27, 2007, Cambridge, Massachusetts, USA
	Philip W. L. Fong, Reasoning about safety properties in a JVM-like environment, Science of Computer Programming, v.67 n.2-3, p.278-300, July, 2007
	Hongxu Cai , Zhong Shao , Alexander Vaynberg, Certified self-modifying code, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Louis-Julien Guillemette , Stefan Monnier, Type-Safe Code Transformations in Haskell, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.23-39, June, 2007
	Boris Feigin , Alan Mycroft, Jones optimality and hardware virtualization: a report on work in progress, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA
	Elvira Albert , Samir Genaim , Miguel Gomez-Zamalloa, Heap space analysis for java bytecode, Proceedings of the 6th international symposium on Memory management, October 21-22, 2007, Montreal, Quebec, Canada
	Dries Vanoverberghe , Frank Piessens, Supporting Security Monitor-Aware Development, Proceedings of the Third International Workshop on Software Engineering for Secure Systems, p.2, May 20-26, 2007
	Chun-Xiao Lin , Yi-Yun Chen , Long Li , Bei Hua, Garbage collector verification for proof-carrying code, Journal of Computer Science and Technology, v.22 n.3, p.426-437, May 2007
	Gianluigi Ferrari , C. Montangero , L. Semini , S. Semprini, Mark, a Reasoning Kit for Mobility, Automated Software Engineering, v.9 n.2, p.137-150, April 2002
	Anindya Banerjee , David A. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, v.15 n.2, p.131-177, March 2005
	Yasuyuki Tsukada, Interactive and Probabilistic Proof of Mobile Code Safety, Automated Software Engineering, v.12 n.2, p.237-257, April 2005
	V. A. Nepomniaschy, Symbolic method of verification of definite iterations over altered data structures, Programming and Computing Software, v.31 n.1, p.1-9, January 2005
	Ajay Chander , David Espinosa , Nayeem Islam , Peter Lee , George C. Necula, Enforcing resource bounds via static verification of dynamic checks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.28-es, August 2007
	V. A. Nepomniaschy, Verification of finite iterations over collections of variable data structures, Cybernetics and Systems Analysis, v.43 n.3, p.341-352, May 2007
	Louis-Julien Guillemette , Stefan Monnier, A type-preserving closure conversion in haskell, Proceedings of the ACM SIGPLAN workshop on Haskell workshop, September 30-30, 2007, Freiburg, Germany
	Andrew W. Appel , Amy P. Felty, Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf, Theory and Practice of Logic Programming, v.4 n.2, p.1-39, January 2004
	Greg Morrisett , Karl Crary , Neal Glew , David Walker, Stack-based typed assembly language, Journal of Functional Programming, v.12 n.1, p.43-88, January 2002
	Steve Zdancewic , Andrew C. Myers, Secure Information Flow via Linear Continuations, Higher-Order and Symbolic Computation, v.15 n.2-3, p.209-234, September 2002
	Aarne Ranta, Grammatical Framework, Journal of Functional Programming, v.14 n.2, p.145-189, March 2004
	Peter Thiemann, Program specialization for execution monitoring, Journal of Functional Programming, v.13 n.3, p.573-600, May 2003
	Thomas E. Hart , Marsha Chechik , David Lie, Security benchmarking using partial verification, Proceedings of the 3rd conference on Hot topics in security, p.1-6, July 29, 2008, San Jose, CA
	Dorina Ghindici , Gilles Grimaud , Isabelle Simplot-Ryl, Embedding verifiable information flow analysis, Proceedings of the 2006 International Conference on Privacy, Security and Trust: Bridge the Gap Between PST Technologies and Business Services, October 30-November 01, 2006, Markham, Ontario, Canada
	Aaron Stump , Morgan Deters , Adam Petcher , Todd Schiller , Timothy Simpson, Verified programming in Guru, Proceedings of the 3rd workshop on Programming languages meets program verification, January 20-20, 2009, Savannah, GA, USA
	Lieven Desmet , Wouter Joosen , Fabio Massacci , Pieter Philippaerts , Frank Piessens , Ida Siahaan , Dries Vanoverberghe, Security-by-contract on the .NET platform, Information Security Tech. Report, v.13 n.1, p.25-32, January, 2008
	Juan Chen , Chris Hawblitzel , Frances Perry , Mike Emmi , Jeremy Condit , Derrick Coetzee , Polyvios Pratikaki, Type-preserving compilation for large-scale optimizing object-oriented compilers, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Yuji Chiba, Java heap protection for debugging native methods, Science of Computer Programming, v.70 n.2-3, p.149-167, February, 2008
	Gang Tan , Greg Morrisett, Ilea: inter-language analysis across java and c, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Marius Nita , Dan Grossman , Craig Chambers, A theory of platform-dependent low-level software, ACM SIGPLAN Notices, v.43 n.1, January 2008
	John Criswell , Andrew Lenharth , Dinakar Dhurjati , Vikram Adve, Secure virtual architecture: a safe execution environment for commodity operating systems, ACM SIGOPS Operating Systems Review, v.41 n.6, December 2007
	A. Prasad Sistla , V. N. Venkatakrishnan , Michelle Zhou , Hilary Branske, CMV: automatic verification of complete mediation for java virtual machines, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan
	Aytekin Vargun , David R. Musser, Code-carrying theory, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil
	Sunae Seo , Hongseok Yang , Kwangkeun Yi , Taisook Han, Goal-directed weakening of abstract interpretation results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.39-es, October 2007
	Ines Margaria , Maddalena Zacchi, Access control in mobile ambient calculi: A comparative view, Theoretical Computer Science, v.398 n.1-3, p.183-202, May, 2008
	Úlfar Erlingsson , Martín Abadi , Michael Vrable , Mihai Budiu , George C. Necula, XFI: software guards for system address spaces, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
	E. Albert , P. Arenas , S. Genaim , G. Puebla , D. Zanardini, Removing useless variables in cost analysis of Java bytecode, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil
	Ando Saabas , Tarmo Uustalu, Type Systems for Optimizing Stack-based Code, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.1, p.103-119, July, 2007
	Jason Reed, Redundancy Elimination for LF, Electronic Notes in Theoretical Computer Science (ENTCS), 199, p.89-106, February, 2008
	Chris Lesniewski-Laas , Bryan Ford , Jacob Strauss , Robert Morris , M. Frans Kaashoek, Alpaca: extensible authorization for distributed services, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA
	Amy P. Felty, Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code, Fundamenta Informaticae, v.77 n.4, p.303-330, December 2007
	Aleksandar Nanevski , Greg Morrisett , Avraham Shinnar , Paul Govereau , Lars Birkedal, Ynot: dependent types for imperative programs, ACM SIGPLAN Notices, v.43 n.9, September 2008
	Sandip Ray , Warren A. Hunt, Jr. , John Matthews , J. Strother Moore, A Mechanical Analysis of Program Verification Strategies, Journal of Automated Reasoning, v.40 n.4, p.245-269, May 2008
	Timothy J. Smith , Lavanya Ramakrishnan, Joint Policy Management and Auditing in Virtual Organizations, Proceedings of the 4th International Workshop on Grid Computing, p.117, November 17-17, 2003
	Fabio Massacci , Ida S. R. Siahaan, Simulating midlet's security claims with automata modulo theory, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, June 07-13, 2008, Tucson, AZ, USA
	Holger Schmidt , Franz J. Hauck, SAMProc: middleware for self-adaptive mobile processes in heterogeneous ubiquitous environments, Proceedings of the 4th on Middleware doctoral symposium, p.1-6, November 26-30, 2007, Newport Beach, California
	Gilles Grimaud , Yann Hodique , Isabelle Simplot-Ryl, On the use of metatypes for safe embedded operating system extension, International Journal of Parallel, Emergent and Distributed Systems, v.22 n.1, p.1-13, January 2007
	Irem Aktug , Katsiaryna Naliuka, ConSpec – A formal language for policy specification, Science of Computer Programming, v.74 n.1-2, p.2-12, December, 2008
	Louis-Julien Guillemette , Stefan Monnier, A type-preserving compiler in Haskell, ACM SIGPLAN Notices, v.43 n.9, September 2008
	Davide Ancona , Sonia Fagorzi , Elena Zucca, A Parametric Calculus for Mobile Open Code, Electronic Notes in Theoretical Computer Science (ENTCS), v.192 n.3, p.3-22, November, 2008
	Andreas Gampe , Jeffery von Ronne , David Niedzielski , Kleanthis Psarris, Speculative improvements to verifiable bounds check elimination, Proceedings of the 6th international symposium on Principles and practice of programming in Java, September 09-11, 2008, Modena, Italy
	Peter C. Chapin , Christian Skalka , X. Sean Wang, Authorization in trust management: Features and foundations, ACM Computing Surveys (CSUR), v.40 n.3, p.1-48, August 2008
	Avik Chaudhuri , Prasad Naldurg , Sriram Rajamani, A type system for data-flow integrity on Windows Vista, ACM SIGPLAN Notices, v.43 n.12, December 2008
	Adam Chlipala, Modular development of certified program verifiers with a proof assistant1,2, Journal of Functional Programming, v.18 n.5-6, p.599-647, September 2008
	Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Hoare type theory, polymorphism and separation1, Journal of Functional Programming, v.18 n.5-6, p.865-911, September 2008
	Aaron Stump , Duckki Oe, Towards an SMT proof format, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, July 07-14, 2008, Princeton, New Jersey
	Jeremy Condit , Brian Hackett , Shuvendu K. Lahiri , Shaz Qadeer, Unifying type checking and property checking for low-level code, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Chris Hawblitzel , Erez Petrank, Automated verification of practical garbage collectors, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Dong-Xi Liu, CSchema: a downgrading policy language for XML access control, Journal of Computer Science and Technology, v.22 n.1, p.44-53, January 2007
	Avik Chaudhuri, Language-based security on Android, Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, June 15-21, 2009, Dublin, Ireland
	Jaime Niño, An overview of programming language based security, Proceedings of the 47th Annual Southeast Regional Conference, March 19-21, 2009, Clemson, South Carolina
	Jan Olaf Blech , Michaël Périn, Certifying deadlock-freedom for BIP models, Proceedings of th 12th International Workshop on Software and Compilers for Embedded Systems, April 23-24, 2009, Nice, France
	Dries Vanoverberghe , Frank Piessens, Security enforcement aware software development, Information and Software Technology, v.51 n.7, p.1172-1185, July, 2009
	Fei Yan , Philip W. L. Fong, Efficient IRM enforcement of history-based access control policies, Proceedings of the 4th International Symposium on Information, Computer, and Communications Security, March 10-12, 2009, Sydney, Australia
	Gaël Thomas , Nicolas Geoffray , Charles Clément , Bertil Folliot, Designing highly flexible virtual machines: the JnJVM experience, Software—Practice & Experience, v.38 n.15, p.1643-1675, December 2008
	Xavier Leroy, Formal verification of a realistic compiler, Communications of the ACM, v.52 n.7, July 2009
	Lujo Bauer , Limin Jia , Michael K. Reiter , David Swasey, xDomain: cross-border proofs of access, Proceedings of the 14th ACM symposium on Access control models and technologies, June 03-05, 2009, Stresa, Italy
	Pieter Hooimeijer , Westley Weimer, A decision procedure for subset constraints over regular languages, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Long Li , Yu Zhang , Yi-Yun Chen , Yong Li, Certifying concurrent programs using transactional memory, Journal of Computer Science and Technology, v.24 n.1, p.110-121, January 2009
	M. Alba-Castro , M. Alpuente , S. Escobar , P. Ojeda , D. Romero, A Tool for Automated Certification of Java Source Code in Maude, Electronic Notes in Theoretical Computer Science (ENTCS), 248, p.19-29, August, 2009
	Nadeem Abdul Hamid, Certified code development for a microcontroller architecture, Proceedings of the 46th Annual Southeast Regional Conference on XX, March 28-29, 2008, Auburn, Alabama
	Massimo Bartoletti , Pierpaolo Degano , Gian-Luigi Ferrari , Roberto Zunino, Local policies for resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.6, p.1-43, August 2009
	Jean-Yves Moyen, Resource control graphs, ACM Transactions on Computational Logic (TOCL), v.10 n.4, p.1-44, August 2009
	P. Parrend , S. Frenot, Security benchmarks of OSGi platforms: toward Hardened OSGi, Software—Practice & Experience, v.39 n.5, p.471-499, April 2009
	Gilles Barthe , Benjamin Grégoire , César Kunz , Tamara Rezk, Certificate translation for optimizing compilers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.5, p.1-45, June 2009