Matt Wilding Talks and Publications

  • David S. Hardin, Raymond J. Richards, and Matthew M. Wilding, High assurance guard for security applications utilizing authentication and authorization services for sources of network data, U.S. Patent 8881260, November 4, 2014.

  • Mark A. Bortz, Matthew M. Wilding, James A. Marek, David S. Hardin, T. Douglas Hiratzka, and Philippe M. T. Limondin, High Assurance Architecture for Routing of Information Between Networks of Differing Security Level, U.S. Patent 8161529, April 17, 2012.

  • David S. Hardin, David A. Greve, Sung J. Kim, and Matthew M. Wilding, Evaluatable High-Assurance Guard for Security Applications, U.S. Patent 7606254, October 20, 2009.

  • David Greve, Raymond Richards, and Matthew Wilding, "Formal Verification of AAMP7 Intrinsic Partitioning", NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, Md., April 13-15, 2004. (talk)

  • David Greve and Matthew Wilding, "Typed ACL2 Records", Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003), Boulder, CO, July 2003. (workshop, paper(pdf), paper(ps), code)

  • David Greve and Matthew Wilding, "Using MBE to Speed a Verified Graph Pathfinder", Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003), Boulder, CO, July 2003. (workshop, paper(pdf), paper(ps), code)

  • David Greve, Matthew Wilding, and W. Mark Vanfleet, "A Separation Kernel Formal Security Policy", Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003), Boulder, CO, July 2003. (workshop, paper(pdf), paper(ps), code)

  • Matthew Wilding, David Greve, John Launchbury, and Peter White, "A High Assurance Partitioned Development Environment", NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, Md., April 1-3, 2003. (abstract, talk)

  • David Greve and Matthew Wilding, "vFaat: von Neumann Formal Analysis and Annotation Tool", NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, Md., April 1-3, 2003. (paper, talk)

  • David Greve and Matt Wilding, "Dynamic Datastructures in ACL2: A Challenge", Nov 2002. (short note)

  • John K. Gee, David A. Greve, David S. Hardin, Allen P. Mass, Michael H. Masters, Nick M. Mykris, and Matthew M. Wilding, Real time processor capable of concurrently running multiple independent JAVA machines, U.S. Patent 6,374,286, April 16, 2002. (patent)

  • David Greve and Matthew Wilding, "Evaluatable, High-Assurance Microprocessors", NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, Md., March 6-8, 2002. (paper, talk)

  • Matthew Wilding, Solution to a challenge problem involving a Mostek 6502 multiplication routine, January 2002. (ACL2 input)

  • Matthew Wilding, David Greve, David Hardin, Efficient Simulation of Formal Processor Models, Formal Methods in Systems Design, 18(3), Kluwer Academic Publishers, May 2001. (journal webpage)

  • Matthew Wilding, An ACL2 solution to Moore's Thread Problem, May 2001. (ACL2 input)

  • Matthew Wilding, "Using a Single-Threaded Object to Speed a Verified Graph Pathfinder", ACL2 Workshop 2000, Austin, TX, October 2000. (workshop, paper)

  • David Greve and Matthew Wilding, "Two Handy update-nth Equality Rules", September 2000. (short note) (paper)

  • David Greve and Matthew Wilding, "Executable Formal Models for Validation and Specless Verification", 19th Digital Avionics Systems Conference (DASC), Philadelphia, PA, October 2000. (conference, paper)

  • David Greve, Matthew Wilding, Mark Bickford, and David Guaspari, "Orpheus: A Self-Checking Translation Tool Arrangement for Flight Critical Hardware Development", Langley Formal Methods 2000 -- LFM00. (conference, paper)

  • David Greve, Matthew Wilding, and David Hardin, "High-Speed, Analyzable Simulators", invited chapter in Using the ACL2 Theorem Prover: A Tutorial Introduction and Case Studies, Kluwer Academic Publishers, July 2000. (chapter)

  • David Jensen, David Greve, and Matthew Wilding, "Secure Reconfigurable Computing" presented to 2nd Annual Military and Aerospace Applications of Programmable Devices and Technologies Sept. 1999. (conference, paper)

  • David Hardin, David Greve, Matthew Wilding, and John Cowles, "Single-Threaded Processor Models: Enabling Proof and High-Speed Execution" presented to 1999 ACL2 Workshop, Austin Tx., Mar 1999. (slides, draft paper)

  • David Greve, Matthew Wilding, and David Hardin, "Suggested ACL2 Enhancements", presented to 1999 ACL2 Workshop, Austin Tx., Mar 1999. (slides)

  • Steve Miller, David Greve, Matthew Wilding, and Mandayam Srivas, "Formal Verification of the AAMP-FV Microcode", NASA Report NASA/CR-1999-208992, Feb 1999. ( ftp://techreports.larc.nasa.gov/pub/techreports/larc/1999/cr/NASA-99-cr208992.pdf)

  • Matthew Wilding, David Hardin, and David Greve, "Invariant Performance: A Statement of Task Isolation Useful for Embedded Application Integration", Dependable Computing for Critical Applications -- DCCA-7, Charles Weinstock and John Rushby (eds.), IEEE Computer Society Dependable Computing Series, 1999. (conference, paper)

  • Matthew Wilding, "A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy", Computer-Aided Verification -- CAV '98, Vancouver Canada, Springer-Verlag Lecture Notes in Computer Science volume 1427, 1998. (paper)

  • David Hardin, Matthew Wilding, and David Greve, "Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle", Computer-Aided Verification -- CAV '98, Vancouver Canada, Springer-Verlag Lecture Notes in Computer Science volume 1427, 1998. (Invited paper) (paper)

  • David Greve and Matthew Wilding, "The World's First Java Processor", January 1998. (Appears as "Stack-based Java a back-to-future step", Electronic Engineering Times, 12 January 1998) (article)

  • Matthew Wilding, "Formal Verification at Rockwell Collins" Presented at Computer Science department colloquia at the University of Texas at Austin and The University of Iowa, January 1998. (slides)

  • Matthew Wilding, "Robust Computer System Proofs in PVS", In LFM97: Fourth NASA Langley Formal Methods Workshop, C. Michael Holloway and Kelly J. Hayhurst, eds. NASA Conference Publication no. 3356, 1997. (conference, slides, paper)

  • Matthew Wilding, "Machine-Checked Real-Time System Verification", Ph.D. Th., University of Texas at Austin, May 1996. University Microfilms, ( ftp://ftp.cs.utexas.edu/pub/boyer/diss/wilding.ps.Z, and ftp://ftp.cs.utexas.edu/pub/boyer/diss/wilding-diss-events.tar)

  • Matthew Wilding, "A Detailed Processor Model for Verification of Real-Time Applications", In T. Hilburn, G. Suski, and J. Zalewski, Ed., 2nd IFAC Workshop on Safety and Reliability in Emerging Control Technologies, Pergamon/Elsevier Science, 1996. (paper)

  • Matthew Wilding, "A Mechanically Verified Application for a Mechanically Verified Environment", Computer-Aided Verification -- CAV '93, Springer-Verlag Lecture Notes in Computer Science volume 697, 1993. (ftp.cs.utexas.edu/pub/boyer/nqthm/wilding-cav93.ps)

  • Matthew Wilding, "Proving Matijasevich's Lemma with a Default Arithmetic Strategy", Journal of Automated Reasoning 7, 3 (1991), Kluwer Academic Publishers.

  • Matthew Wilding, "A Mechanically-Checked Correctness Proof of a Floating-Point Search Program", Tech. Rept. 56, Computational Logic, Inc., 1990. ( ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/056.ps)

  • Matthew Kaufmann and Matthew Wilding, "A Parallel Version of the Boyer-Moore Theorem-Prover", Tech. Rept. 39, Computational Logic, Inc., 1990. ( ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/039.ps)

  • Matthew Wilding, Scott Rudy, and Catherine Neuswanger, "CGS User's Manual" technical report BDM/W-85-605-TR, BDM Corporation, 1985.

    Back to Wilding Web Page