LCF-style for Secure Verification Platform based on Multiway Decision Graphs

Abstract. Formal verification of digital systems is achieved, today, using one of two main approaches: states exploration (mainly model checking and equivalence checking) or deductive reasoning (theorem proving). Indeed, the combination of the two approaches, states exploration and deductive reasoning promises to overcome the limitation and to enhance the capabilities of each. A comparison between both categories is discussed in details. In this paper, we are interested in presenting as an example a platform for Multiway Decision Graphs (MDGs) in LCF-style theorem prover. Based on this platform, many conversions such as the reachability analysis and reduction techniques can be implemented that uses the MDG theory within the HOL theorem prover. The paper also questions the best formalization principle of decision graphs to build such a platform in theorem proving since a set of basic operations are used to efficiently manipulate the decision graphs which constitute the kernel of the mod...

• Type: Conference
• Year: 2009
• Where: CIIA
• Authors: Sa'ed Abed, Otmane Aït Mohamed
• Keywords: CIIA 2009, Decision Graphs, Deductive Reasoning, Information Technology, Theorem Proving