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).