The Software Correctness and Safety Research Laboratory studies
the application of theorem proving and other related formal techniques
to providing assurance that complex software systems work correctly
Our current research includes the following projects.
Higher-Order Abstract Syntax and InductionLogical frameworks supporting higher-order abstract syntax allow a direct and concise specification of a wide variety of logics, programming languages, and deductive systems. Programming with such specifications is well-supported by languages such as Lambda Prolog and Twelf. Reasoning about such specifications provides the opportunity to establish meta-theory of the encoded languages; it can be used, for example, to formalize the meta-theory of programming languages. Carrying out such reasoning within the same framework as the specifications, however, presents some challenges. Our group is active in developing the Hybrid approach and tool [1, 2, 3, 4, 5, 7, 8], which implements a definitional, multi-level approach  to such reasoning within the Isabelle and Coq proof assistants. In particular, we define higher-order syntax encodings on top of the base level so that they expand to a de Bruijn representation of terms, and provide a library of operations and lemmas to reason on the higher-order syntax which hide the details of the de Bruijn representation. We have also implemented a constructive version of Hybrid in Coq, which includes recursion principles that work directly on the higher-order syntax . In addition, we have developed a generalized version where a large class of theorems that must be repeated for each object language in Hybrid is done once in the new version and can be applied directly to each object language .
 Hybrid: A Definitional Two Level Approach to Reasoning with Higher-Order Abstract Syntax, by Amy Felty and Alberto Momigliano. Journal of Automated Reasoning, 48(1):43-105, 2012, DOI 10.1007/s10817-010-9194-x (SpringerLink, pdf).
 An Improved Implementation and Abstract Interface for Hybrid, by Alan J. Martin, and Amy P. Felty. To appear in Proceedings of the Sixth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), August 2011, (pdf).
 Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study, by Alan J. Martin, Ph.D. thesis, University of Ottawa, November 2010 (pdf).
 Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison, by Amy Felty and Brigitte Pientka. In International Conference on Interactive Theorem Proving, Springer-Verlag LNCS, July 2010 (pdf).
 Higher-Order Abstract Syntax in Type Theory, by Venanzio Capretta and Amy Felty. In Logic Colloquium '06, ASL Lecture Notes in Logic, 32, Cambridge University Press, October 2009 (pdf, Coq formalization, Example application).
 Reasoning with Hypothetical Judgments and Open Terms in Hybrid, by Amy Felty and Alberto Momigliano. In 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, September 2009 (pdf).
 Two-level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax, by Alberto Momigliano, Alan J. Martin, and Amy P. Felty. In Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007), in Electronic Notes in Theoretical Computer Science, 196:85-93, January 2008 (pdf, see  for Isabelle and Coq formalizations)
 Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq, by Venanzio Capretta and Amy Felty. In Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers, Springer-Verlag LNCS 4502, 2007 (pdf, Coq formalization).
 Higher-Order Abstract Syntax in Coq, by Joëlle Despeyroux, Amy Felty, and André Hirschowitz. In Second International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 902, April 1995 (postscript).
 Devera Logic, Inc.
 An Algorithm for Compression of XACML Access Control Policy Sets by Recursive Subsumption, by Bernard Stepien, Amy Felty, and Stan Matwin. Seventh International Conference on Availability, Reliability, and Security, August 2012 (pdf).
 Advantages of a Non-Technical XACML Notation in Role-Based Models, by Bernard Stepien, Stan Matwin, and Amy Felty. In 9th Annual Conference on Privacy, Security, and Trust, July 2011 (pdf).
 Strategies for Reducing Risks of Inconsistencies in Access Control Policies, by Bernard Stepien, Stan Matwin, and Amy Felty. In 5th International Conference on Availability, Reliability, and Security, February 2010 (pdf).
 A Non-technical User-Oriented Display Notation for XACML Conditions, by Bernard Stepien, Amy Felty, and Stan Matwin. In E-Technologies: Innovation in an Open World, Proceedings of the 4th International MCETECH Conference, Springer LNBIP 26, 2009 (pdf).
 Formal Correctness of Conflict Detection for Firewalls, by Venanzio Capretta, Bernard Stepien, Amy Felty, and Stan Matwin. In ACM Workshop on Formal Methods in Security Engineering, November 2007 (pdf, Coq formalization).
 Privacy in Data Mining Using Formal Methods, by Stan Matwin, Amy Felty, Istvan Hernadvolgyi, and Venanzio Capretta. In Seventh International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 3461, April 2005 (pdf).
 Privacy-Oriented Data Mining by Proof Checking, by Amy Felty and Stan Matwin In Sixth European Conference on Principles of Data Mining and Knowledge Discovery, Springer-Verlag LNCS 2431, August 2002 (pdf).
Proof-Carrying CodeProof-carrying code (PCC) provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. The principle advantage is that the trusted computing base is extremely small; it includes only the proof checker for verifying the proof of safety. In addition, the safety properties of interest are much easier to prove automatically than general program correctness. Our current work is on foundational proof-carrying code [22, 25] which provides increased security by decreasing the size of the trusted computing base (TCB), and increased flexibility by allowing a single safety policy to be used for multiple programming languages and compilers. This work is in collaboration with Andrew Appel (Princeton University) and others. Our current work centers around two areas. First, we aim to scale up the approach to fully automate proofs of safety for full programming languages such as ML and Java . Second, we are designing a general environment for implementing foundational proof-carrying code systems [23, 24]. This work is part of a more general effort on the design and implementation of a system which provides a uniform framework for developing programming languages and proving properties about them, and for writing, interpreting, debugging, and proving properties of programs written in these languages.
 An Implementation of a Verification Condition Generator for Foundational Proof-Carrying Code by Jiangong Weng and Amy Felty. In 9th Annual Conference on Privacy, Security, and Trust, July 2011, (pdf).
 Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code, by Amy P. Felty. Fundamenta Informaticae, 7(4):303-330, 2007 (pdf).
 Dependent Types Ensure Partial Correctness of Theorem Provers, by Andrew W. Appel and Amy P. Felty. Journal of Functional Programming, 14(1):3-19, January 2004 (postscript).
 Polymorphic Lemmas and Definitions in Lambda Prolog and Twelf, by Andrew W. Appel and Amy P. Felty. Theory and Practice of Logic Programming, 4(1&2):1-39, January & March 2004 (pdf).
 A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, by Andrew W. Appel and Amy P. Felty. In The 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2000 (postscript).
Genetic Programming with Polymorphic Types and Higher-Order FunctionsWe are developing a new approach to program representation for genetic programming (GP), replacing the usual s-expression representation scheme with programs in the higher-order polymorphically typed language System F [26, 27]. As a result of the expressive power of this calculus, the system is able to express programming structures such as recursion and data types without explicit definitions. Using such a system, we are able to evolve programs that exhibit recursive behavior without explicitly defining recursion-specific syntax in the terminal set. This work can be viewed as an approach to inductive programming.
 Genetic Programming with Polymorphic Types and Higher-Order Functions, by Franck Binard and Amy Felty. In Proceedings of the Tenth Annual Conference on Genetic and Evolutionary Computation, ACM Press, 2008 (pdf).
 An Abstraction-Based Genetic Programming System, by Franck Binard and Amy Felty. In Genetic and Evolutionary Computation Conference: Late Breaking Papers, 2007 (pdf).
Research Scientists and Postdocs: