Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] on formalization of predicate abstraction in I...

view this post on Zulip Email Gateway (Aug 22 2022 at 19:40):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:
Do you know who have done formalization in Isabelle or other theorem prover
for predicate abstraction in advanced model checking theory, and
prove that the abstarcted system
can simulates the original system?

Thanks in advance

regards!

Associate Professor
State Key Laboratory of Computer Science,
Institute of Software,
Chinese Academy of Sciences
P.O. Box 8718
Beijing 100190
CHINA

Tel. (86) (10) 62661645
E-mail: lyj238@ios.ac.cn

view this post on Zulip Email Gateway (Aug 22 2022 at 19:40):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:
Do you know who have done formalization in Isabelle or other theorem prover
for predicate abstraction in advanced model checking theory, and
prove that the abstarcted system
can simulates the original system?

Thanks in advance

regards!

Associate Professor
State Key Laboratory of Computer Science,
Institute of Software,
Chinese Academy of Sciences
P.O. Box 8718
Beijing 100190
CHINA

Tel. (86) (10) 62661645
E-mail: lyj238@ios.ac.cn

Last updated: Apr 26 2024 at 12:28 UTC