a) higher-order logic
b) higher-order last
c) highly organized logic
d) higher-order less
Answer: a
The formal verification techniques are classified based on the logic employed. The techniques are propositional logic, first-order logic, and higher-order logic. The HOL is the abbreviation of the higher-order logic in which the proofs are automated and manually done with some proof support.
22. What is BDD?
a) boolean decision diagram
b) binary decision diagrams
c) binary decision device
d) binary device diagram
Answer: b
The binary decision diagram is a kind of data structure that is used to represent the Boolean function.
23. Which formal verification technique consists of a Boolean formula?
a) HOL
b) FOL
c) Propositional logic
d) Both HOL and FOL
Answer: c
The propositional logic technique is having the boolean formulas and the boolean function. The tools used in propositional logic are the tautology checker or the equivalence checker which in turn uses the binary decision diagrams which are also known as BDD.
24. Which of the following is also known as an equivalence checker?
a) BDD
b) FOL
c) Tautology checker
d) HOL
Answer: c
The propositional logic technique consists of the boolean formulas and the boolean function. The tools used in this type of logic are the tautology checker or the equivalence checker which in turn uses the BDD or the binary decision diagrams.
25. Which of the following is possible to locate errors in the specification of the future bus protocol?
a) EMC
b) HOL
c) BDD
d) FOL
Answer: c
The model checking was developed using the binary decision diagram and the BDD and it was possible to locate errors in the specification of the future bus protocol.
26. Which of the following is a popular system for model checking?
a) HOL
b) FOL
c) BDD
d) EMC
Answer: d
The EMC system is developed by Clark and it describes the CTL formulas, which is the computational tree logic.
27. What is CTL?
a) computational tree logic
b) code tree logic
c) CPU tree logic
d) computer tree logic
Answer: a
The EMC-system is a popular system for model checking which is developed by Clark that describes the CTL formulas, which is also known as computational tree logic. The CTL consists of two parts, a path quantifier, and a state quantifier.
