Selected Publications

• Fritz, A. and P. Alexander, “Policy-based Attestation Protocol Negotiation,” NASA Formal Methods Symposium (NFM’23), Houston, TX, May 16-18, 2023.

• Petz, A. and P. ALexander, “Formally verified bundling and appraisal of evidence for layered attestations,” Innovations in Systems and Software Engineering, https://doi.org/10.1007/s11334-022-00475-1, September 2022.

• Helble, S., I. Kretz, P. Loscocco, J. Ramsdell, P. Rowe, and P. Alexander “Flexible Mechanisms for Remote Attestation,” ACM Transactions On Security and Privacy, 24(4), September 2021.

• Petz, A., G. Jurgensen, and P. Alexander, “Design and Formal Verification of a Copland-based Attestation Protocol,” ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE’21), Virtual, Nov 20-22, 2021.

• Petz, A. and P. Alexader, “An Infrastructure for Faithful Execution of Remote Attestation Protocols,” NASA Formal Methods Symposium (NFM’21), May 24-28, 2021, Norfolk, VA.

• Petz, A. and P. Alexander, “A Copland Attestation Manager,” Hot Topics in Science of Security (HoTSoS’19), Nashville, TN, April 8-11 2019.

• Ramsdell, J., P. D. Rowe, P. Alexander, S. Helble, P. Loscocco, J. A. Pendergrass, and A. Petz, “Orchestrating Layered Attestations,” Principles of Security and Trust (POST’19), Prague, Czech Republic, April 8-11, 2019.

• Borck, H., P. Kline, H. Shackleton, J. Gohde, S. Johnston, P. Alexander, and T. Carpenter, “100 Years of Software – Adapting Cyber-Physical Systems to the Changing World,” Software Engineering for Resilient Systems (SERENE’17), Geneva, Switzerland, September 4-5, 2017.

• Alexander, P., L. Pike, P. Loscocco, G. Coker, “Model Checking Distributed Mandatory Access Control Policies,” in ACM Transactions on Information and System Security (TISSEC) 2(18), 2015.

• Austin, E. and P. Alexander, “Challenges Implementing an LCF-Style Proof System with Haskell,” in Proceedings of the International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS’15), Austin, Texas USA, September 26-27, 2015.

• Austin, E. and P. Alexander, “Stateless Higher-Order Logic with Quantified Types,” International Conference on Interactive Theorem Proving (ITP’13), LNCS 7998, Rennes, France, July 2013.

• Halling, B., and P. Alexander, “Verifying a Privacy CA Remote Attestation Protocol,” NASA Formal Methods Conference (NFM’13), LNCS 7871, Mountain View, CA, May 2013.

• Frisby, N., A. Gill and P. Alexander, “A Pattern for Almost Homomorphic Functions,” The ACM SIGPLAN Workshop on Generic Programming (WGP’12), Copenhagen, Denmark, September 9-10, 2012.

• Haricombe, L. J., L. A. Emmett, and P. Alexander, “Open Access: An Evolving Alternative,” IEEE Computer, 45(8), August 2012, pp. 70-72.

• Peck, M. and P. Alexander, “Rosetta Composition Semantics,” in Progressions and Innovations in Model-Driven Software Engineering, V. G. Díaz, J. M. C. Lovelle, B. C. P. Garcia-Bustelo, and O. S. Martinez, Editors, IGI Global, in press.

• Kimmell, G., W. Peck, and P. Alexander, “System Development with Oread,” 2011 Symposium on Implementation and Application of Functional Langauges (IFL’11), Lawrence, KS, 2011.

• Austin, E., and P. Alexander, “Haskell + HOL = HaskHOL,” 2011 Symposium on Implementation and Application of Functional Langauges (IFL’11), Lawrence, KS, 2011.

• Frisby, N., M. Peck, M. Snyder, P. Alexander, “Model Composition in Rosetta,” IEEE Engineering of Computer-Based Systems Symposium and Workshops, (ECBS’11), Las Vegas, NV, 2011.

• Austin, E., and P. Alexander, “HaskHOL: A Haskell Hosted Domain Specific Language Representation of HOL Light,” Trends in Functional Programming (TFP’10), Norman, OK, May 17-19, 2010.

• Snyder, M., and P. Alexander, “Type-Indexed Monads,” Trends in Functional Programming (TFP’10), Norman, OK, May 17-19, 2010.

• Kimmell, G., N. Frisby, P. Weaver, and P. Alexander, “Constructing Language Processors with Algebra Combinators,” Science of Computer Programming, 75(7), July, 2010.

• Alexander, P., “Rosetta: Standardization at the System Level,” IEEE Computer, 42(1), January 2009

• Snyder, M., N. Frisby, G. Kimmell, P. Alexander, “Writing Composable Software with InterpreterLib,” Proceedings of Software Composition (SC’09), Zurich, Switzerland, July 2-3, 2009.

• Kimmell, G., E. Komp, G. Minden, and P. Alexander, “Synthesizing Software Defined Radios from Rosetta Specifications,” Proceedings of the Forum on specification and Design Languages (FDL’08),Stuttgart, Germany, September 23-25, 2008

• Kimmell, G., E. Komp, and P. Alexander, “Mutli-target Synthesis from a Monadic Specification Language,” Proceedings of the Emerging Technologies and Factory Automation (ETFA’08) , Hamburg, Germany, September 15-18, 2008

• Alexander, P., “Security as a System-Level Constraint,” invited presentation at Google Tech Talks , Mountain View, CA, June 4, 2008

• Alexander, P., “Security as a System-Level Constraint,” invited presentation at High Confidence Systems and Software Symposium (HCSS’08) , Baltimore, MD, March 3, 2008

• Alexander, P., “A Tutorial Introduction to Rosetta Semantics,” tutorial presentation at the Forum on specification and Design Languages (FDL’08), Stuttgart, Germany, September 23-25, 2008

• Weaver, P., Kimmell, G., N. Frisby, and P. Alexander, “Modular and Generic Programming with InterpreterLib” Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE’07), Atlanta, GA, November, 2007

• Weaver, P., G. Kimmell, N. Frisby, and P. Alexander, “Constructing Language Processors with Algebra Combinators,” Proceedings of the Generative Programming and Component Engineering (GPCE’07), Salzburg, Austria, October, 2007

• Streb, J., G. Kimmell, N. Frisby, P. Alexander, “Domain Specific Model Composution Using A Lattice Of Coalgebras,” Proceedings of the OOPSLA Workshop on Domain Specific Modeling, Portland, OR, October, 2006

• Streb, J. and P. Alexander, “Using a Lattice of Coalgebras For Heterogeneous Model Composition,” Proceedings of the MoDELS Workshop on Multi-Paradigm Modeling, Genova, Italy, October 3, 2006

• Alexander, P., System Level Design with Rosetta, Morgan Kaufmann Publishers, Sept 2006

• Ward, J., G. Kimmell, and P. Alexander, “Prufrock: A Framework for Constructing Polytypic Theorem Provers,” Proceedings of the 20th International Conference on Automated Software Engineering (ASE’05), Long Beach, CA, 2005

• Kimmell, G., E. Komp and P. Alexander, “Building Compilers by Combining Algebras,” Proceedings of the IEEE Engineering of Computer-Based Systems Symposium and Workshop (ECBS’05), Washington, DC, April 4-7, 2005

• Morel, B. and P. Alexander, “SPARTACAS: Automating Component Reuse and Adaptation,” IEEE Transactions on Software Engineering, 30(9)

• Andrews, D. and P. Alexander, “Laboratory Support for MIPS-style Processor Design,” supplement to Computer Organization and Design, 3rd Edition, by David Patterson and John Hennessey, Morgan Kaufmann, 2004

• Kimmell, G. and P. Alexander, “Modular Monadic Semantics for Aspect Oriented Programs,” poster presentation at the ACM International Conference on Functional Programming, Snowbird, UT, September 19-22, 2004

• Zinjuwadia, K. and P. Alexander, “DVTG and Test Harnessing Using Rosetta Specifications,” Proceedings of the 11th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS’04), Brno, Czech Republic, May 24-26, 2004

• Kong, C., P. Alexander, and C. Menon, “Defining a Formal Coalgebraic Semantics for The Rosetta Specification Language,” Journal of Universal Computer Science, 9(11)

• Morel, B. and P. Alexander, “Automating Component Adaptation for Reuse,” Proceedings of the Automated Software Engineering Conference (ASE’03), Montreal, Quebec, Canada, October 2003

• Kong, C. and P. Alexander, “Defining a Formal Semantics for the Rosetta Specification Language,” Proceedings of the IFIP Formal Specification of Computer-Based Systems Workshop (FSCBS’03), Huntsville, AL, April 2003

• Morel, B. and P. Alexander, “A Slicing Approach for Parallel Component Adaptation,” Proceedings of the IEEE Engineering of Computer-Based Systems Symposium and Workshop (ECBS’03), Huntsville, AL, April 7-10, 2003

• Kong, C. and P. Alexander, “The Rosetta Meta-Model Framework,” Proceedings of the IEEE Engineering of Computer-Based Systems Symposium and Workshop (ECBS’03), Huntsville, AL, April 7-11, 2003

• Kong, C. and P. Alexander, “Multi-Faceted Requirements Modeling and Analysis,” Proceedings of the IEEE Joint International Requirements Engineering Conference (RE’02), Essen, Germany, Septebmer 9-13, 2002

• Kong, C. and P. Alexander, “Modeling Model of Computation Ontologies in Rosetta,” Proceedings of the Formal Specification of Computer Based Systems (FSCBS’02), Lund, Sweden, April 10-11, 2002

• Alexander, P. and C. Kong, “Synthesis as Retrieval: Feature-Based Retrieval and Adaptation Architectures,” Proceedings of the AAAI 2002 Spring Symposium Series, Workshop on Logic-Based Program Synthesis, Stanford University, March 25-27, 2002

• Murali, R., K. Jambhekar, A. Rajkhowa, and P. Alexander, “VSPEC and its Integrated Tool Suite,” Proceedings of the 9th IEEE Engineering of Computer-Based Systems Symposium and Workshop, Lund, Sweden, April 8-11, 2002

• Frey, P. and R. Radhakrishnan, H. Carter, P. Alexander, and P. Wilsey, “A Formal Specification and Verification Framework for Time Warp Based Parallel Simulation,” IEEE Transactions on Software Engineering, 28(1) , pp. 58-78

• Alexander, P. and C. Kong, “Rosetta: Semantic Support for Model-centered Systems Level Design,” IEEE Computer, 34(11) , pp. 64-70

• Akkipeddi, S., P. Alexander, K. Ranganathan, and P. Chawla, “Generating Test Vectors from Systems Requirements,” Proceedings of the Procedings of AutoTestCon’01, Washington, DC, May, 2001

• Cindy Kong and Perry Alexander, “Heterogeneous Computer-Based System Specification,” Proceedings of the Formal Specification of Computer-Based Systems Workshop, Washington, DC, April 20, 2001

• Alexander, P., C. Kong and D. Schonberger, “A Practical Semantics for Domain Interaction,” Proceedings of the Engineering of Computer Based Systems Symposium and Workshop (ECBS’01), Washington, DC, April, 2001

• Chawla, P. and P. Alexander, “Automated Reuse Support for Design of Embedded Avionics Systems,” Proceedings of the IEEE Aerospace Conference, March, 2001

• Alexander, P. and D. Barton, “A Tutorial Introduction to Rosetta,” Proceedings of the Hardware Description Languages Conference (HDLCon’01), San Jose, CA, March 2001

• Perry Alexander, Roshan Kamath, and David Barton, “System Specification in Rosetta,” Proceedings of the IEEE Engineering of Computer Based Systems Symposium, Edinburgh, UK, April 2000

• Murali Rangarajan, Perry Alexander, et. al., “On the Design of Orbit,” Proceedings of the IEEE Engineering of Computer Based Systems Symposium, Edinburgh, UK, April 2000

• Perry Alexander, Cindy Kong and David Barton, “Rosetta Functional Specification Domains,” Proceedings of HDLCon’00, San Jose, CA, March, 2000

• Perry Alexander, “Introuction to Theorem Proving in Higher Order Logic,” tutorial presentation at Theorem Proving in Higher-Order Logic (TPHOL’00), Porland, OR, August, 2000

• Makarand Patil and Perry Alexander, “A Component Retrieval System Using PVS,” poster presentation at Theorem Proving in Higher-Order Logic (TPHOL’00), Porland, OR, August, 2000

• Cindy Kong, Darryl Dieckman and Perry Alexander, “Formal Modeling of Active Network Nodes Using PVS,” Proceedings of the Formal Methods in Software Processes (FMSP’00), Portland OR, August 2000

• Arun Venkataswaran, Murali Rangarajan, and Perry Alexander, “Composition of Specifications in VSPEC,” Proceedings of the Inernational Conference on Formal Engineering Methods (ICFEM’00), York, England, September, 2000

• Krishna Ranganathan, Murali Rangarajan, Perry Alexander, and Tom Regan, “Design Verification Test Generation from Rosetta Specifications,” Proceedings of the VHDL International User’s Forumd (VIUF’00), Orlando, FL, October 2000

• Peter Ashenden, Perry Alexander and David Barton, “A Dual Spring System Case Study Model in Rosetta,” Proceedings of the Forum On Design Languages (FDL-00), Tubingen, Germany, September 2000

• Praveen Chawla and Perry Alexander, “Enabling Collaboration Through Specification Based Search and Retrieval,” Proceedings of the Collaborative Engineering Workshop, Detroit, MI, November 1999

• Perry Alexander, Roshan Kamath, and David Barton, “Facets and Domains in SLDL,” Proceedings of the Forum On Desgin Languages (FDL-99), Lyon, FR, September 1999

• Roshan Kamath, Perry Alexander, and David Barton, “SLDL: A Systems Level Design Language,” Proceedings of the ASIC/SOC 99, Washington, DC, September 1999

• Perry Alexander, Murali Rangarajan, and Phillip Baraona, “A Brief Summary of VSPEC,” Proceedings of the World Congress on Formal Methods (FM’99), Tolouse, FR, September 1999

• Murali Rangarajan and Perry Alexander, “Application of Proof Obligations in the Design Process,” Proceedings of the International Conference on Software Engineering and Knowledge Engineering (SEKE-99), 1999

• Victoria Chernyakhovsky, Peter Frey, Ramanan Radhakrishnan, Philip A. Wilsey, Perry Alexander and Hal Carter, “A Formal Framework for Specifying and Verifying Time Warp Optimizations,” Proceedings of the Workshop on Formal Methods for Parallal Programming: Theory and Application, April 1999

• Murali Rangarajan, Nael Abu-Ghazaleh, and Perry Alexander, “Using Automatable Proof Obligations for Component-Based Design Checking,” Proceedings of the International Symposium and Workshop on Engineering of Computer-Based Systems (ECBS’99), Nashville, TN, March 1999

• Nael Abu-Ghazaleh, Darryl Dieckman, Murali Rangarajan, Perry Alexander and Philip A. Wilsey, “Orbit: An Environment for Component-Based Heterogeneous Design and Analysis,” Proceedings of the International Symposium and Workshop on Engineering of Computer-Based Systems (ECBS’99), Nashville, TN, March 1999

• Amit Rajkhowa and Perry Alexander, “VSPEC Constraint Modeling and Evaluation,” Proceedings of the International Symposium and Workshop on Engineering of Computer-Based Systems (ECBS’99), Nashville, TN, March 1999

• Peter Frey, Ramanan Radhakrishnan, Philip A. Wilsey, Perry Alexander and Hal Carter, “An Extensible Formal Framework for the Specification and Verification of an Optimistic Simulation Protocol,” Proceedings of the 32nd Hawaii International Conference on System Sciences (HICSS-32), January, 1999