Sciweavers

Share
CIIA
2009

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

9 years 9 months ago
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...
Sa'ed Abed, Otmane Aït Mohamed
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2009
Where CIIA
Authors Sa'ed Abed, Otmane Aït Mohamed
Comments (0)
books