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

摘要: Formal verification of digital systems is achieved, today, using one two main approaches: states exploration (mainly model checking and equivalence checking) or deductive reasoning (theorem proving). Indeed, the combination approaches, promises to overcome limitation enhance capabilities each. A comparison between both categories discussed in details. In this paper, we are interested presenting as an example a platform for Multiway Decision Graphs (MDGs) LCF-style theorem prover. Based on platform, many conversions such reachability analysis reduction techniques can be implemented that uses MDG theory within HOL The paper also questions best formalization principle decision graphs build proving since set basic operations used efficiently manipulate which constitute kernel algorithms, by describing alternatives formalize these graphs. Then contrast them according their efficiency, complexity feasibility. Finally, hope serve adequate introduction concepts involved survey relevant work.