Normalization of Linear Horn Clauses - Formal Methods: Foundations and Applications - page 257

we demonstrated how to solve backward reachability for CDPNs by means of our nor-
malization procedure. We have implemented our algorithm in OC AML . The system
can be downloaded from http://www2.in.tum.de/ ∼ seidl/downloads/H/
Our system also provides support for the Magic set transformation which helps to nar-
row down the least model to those facts which are necessary to answer the query as
well as special support for dealing with ground terms. Preliminary experiments with
cryptographic protocols and dynamic pushdown networks seem promising. As future
work, we want to try our tool on more realistic examples, and also enhance it with
instantiation based on automatic finiteness analysis.

References

[1] Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW,
pp. 82-96. IEEE Computer Society, Los Alamitos (2001)
[2] Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Ap-
plication to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997.
LNCS, vol. 1243, pp. 135-150. Springer, Heidelberg (1997)
[3] Bouajjani, A., Muller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks
of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653,
pp. 473-487. Springer, Heidelberg (2005)
[4] Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Transactions on
Information Theory 29(2), 198-207 (1983)
[5] Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking push-
down systems. Electr. Notes Theor. Comput. Sci. 9 (1997)
[6] Goubault-Larrecq, J.: Personal communication (2003)
[7] Goubault-Larrecq, J.: Deciding H 1 by resolution. Inf. Process. Lett. 95(3), 401-408 (2005)

[8] Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In:
Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363-379. Springer, Heidelberg (2005)
ISBN 3-540-24297-X
[9] Lugiez, D., Schnoebelen, P.: The regular viewpoint on pa-processes. Theor. Comput.
Sci. 274(1-2), 89-115 (2002)
[10] Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Sys-
tems. PhD thesis, Technische Universitat Munchen (1998)
[11] Nielsen, C.R., Nielson, F., Nielson, H.R.: Iterative Specialisation of Horn Clauses. In:
Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 131-145. Springer, Heidelberg
(2008)
[12] Nielson, F., Nielson, H.R., Seidl, H.: Normalizable Horn clauses, strongly recognizable
relations and Spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477,
pp. 20-35. Springer, Heidelberg (2002)
[13] Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In:
Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314-328. Springer, Heidel-
berg (1999) ISBN 3-540-66222-7