A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL

DOI10.1016/j.tcs.2011.01.032zbMath1244.68053OpenAlexW1974676396MaRDI QIDQ541222

Yongjian Li, William N. N. Hung, Xiaoyu Song

Publication date: 6 June 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.01.032

zbMATH Keywords

formal semanticsIsabelle/HOLsymbolic trajectory evaluationclosure semanticsnetlist

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Formalization of function matrix theory in HOL

Uses Software

• ML
• Isabelle/HOL
• reFLect
• Lava

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Isabelle/HOL. A proof assistant for higher-order logic
• A reflective functional language for hardware design and theorem proving
• Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
• Theorem Proving in Higher Order Logics
• Higher Order Logic and Hardware Verification