ITL
© 1996-2018







I.3 ITL’s Influence

ITL’s Influence [Slide 14]

  • ITL helped influence Prof Mike Gordon, FRS to switch from LCF to HOL in his theorem proving tools. (E.g., see his article “From LCF to HOL: A short history”).
  • Hybrid systems: Duration Calculus (real and discrete time).
  • ITL is used to give semantics to Verilog (EPSRC project with Oxford University).
  • ITL is used in hardware/software codesign (EPSRC projects with University of Newcastle upon Tyne and Oxford University).
  • ITL is used for security and trust policies (DTC-DIF projects).
  • ITL used in the projects Safemos (UK) and ProCoS (EU).
  • Mexitl (Kent, Winnipeg) is based on ITL, Multimedia in Executable Interval Temporal Logic.

ITL’s Influence [Slide 15]

  • AnaTempura runtime verification tool uses executable subset of ITL.
  • Influenced Verisity Ltd.’s language temporal e (part of IEEE Standard 1647). Verisity acquired by Cadence Design Systems, Inc., a major supplier of electronic design tools and services.
  • Used in the KIV theorem prover (University of Augsburg, Germany) - e.g., for Statecharts, UML and medical protocols.
  • ITL with framing and temporal projection extensively studied by Duan and group (Xidian University, Xi’an, China).







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL