CAETI Contract Overview
with pointers to Application Meta Data

  Computational Logic, Inc.
  Austin, TX

CAETI Minimal Architecture Specification A model of the Minimal Architecture in ACL2 (infix). Includes extensive pointers to original sources and other documentation.
ACL2 ACL2 is
  • a logic and programming language in which you can model idgital systems and
  • a tool to help you prove properties of those models.
Infix interface for ACL2For those uncomfortable with the Lisp syntax of ACL2, we provide a more conventional infix interface in which guards appear as conventional types. We argue that this logic should be easily adoptable by software engineers, in contrast to other non-constructive, formal systems such as Z or PVS.
Executable Z EZ provides a capability to parse an extended Z file, and generate executable functions corresponding to state changing schema. The subset of Z that we support includes globals, axioms, schemas and types.
Evaluation Agents An example of a real-time evaluation agent in the MOO. In this case it tracks a finite state model of the events involving the student. More generally, such evaluation agents could be used to track adherence of a system to its formal specification. The finite state model allows us to check temporal properties.
This page is URL