Selected Publications

Petz, A., W. Thomas, A. Fritz, T. Barclay, L. Schmalz, and P. Alexander, ``Verified Configuration and Deployment of Layered Attestation Managers,’’ 22nd International Conference on Software Engineering and Formal Methods (SEFM’24), November 4-8, 2024, Aveiro, Portugal.
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 veriﬁed 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, 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, and G. Coker, “Model Checking Distributed Mandatory Access Control Policies,” ACM Transactions on Information and System Security (TISSEC), 18(2), 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 RemoteAttestation Protocol,” NASA Formal Methods Conference (NFM’13), LNCS 7871, Mountain View, CA, May 2013.
Frisby, N., A. Gill and P. Alexander, “A Pattern for AlmostHomomorphic 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. Diaz, 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. 2010
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
Alexander, P., G. Kimmell, and D. Burke, Security as a System Property: Modeling trust and security in Rosetta, technical memo, January 4, 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
Uk’taad B’mal, A Haskell Companion for “Fold and Unfold for Program Semantics”, technical memo, June 15, 2005
Uk’taad B’mal, A Haskell Companion for “Using catamorphisms, subtypes and monad transformers for writing modular functional interpreters,”, technical memo, March 3, 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 and David Barton, “An Introduction to Rosetta,” tutorial presentation at the HDLCon00, San Jose, CA, March, 2000
Perry Alexander, Cindy Kong and David Barton, “Rosetta Functional Specification Domains,” Proceedings of the HDLCon00, San Jose, CA, March, 2000
Perry Alexander, “Introuction to Theorem Proving in Higher Order Logic,” tutorial presentation at the TPHOLs 2000, Porland, OR, August, 2000
Makarand Patil and Perry Alexander, “A Component Retrieval System Using PVS,” poster presentation at the TPHOLs 2000, 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