Seeking advice to resolve server down while autoprove with 256GB RAM

[‍한윤선(대학원생-정보융합보안전공)]

Dear Esteemed Researchers,

My name is Yoonsun Han, and I am a first-semester Ph.D. student studying security protocols at Kookmin University, South Korea.

I am writing to seek your advice regarding an issue I am currently facing. For your reference, I have attached the file I am testing. So far, I have only generated the Lemma for secrecy. I would be very grateful for any guidance you could provide on how to diagnose the cause of the server down.

The specifications of the PC I am using are as follows:

Processor: Intel(R) Xeon(R) W7-3455, 2.50 GHz
RAM: 256GB

I ran the process with the --heuristic=sC option, executing the autoprove for Lemma secrecy for approximately three days. During this time, RAM usage exceeded 90%, but the server eventually went down.

Any advice or suggestions you could offer at your convenience would be greatly appreciated.

Thank you very much for taking the time to read this email.

Best regards,
Yoonsun Han

[Ralf Sasse]

Dear Yoonsun Han,

Generally we would try to run the proof attempt without any --heuristic parameter, defaulting to --heuristic=s. I am not sure why you want to include the C heuristic. Doing this may of course have the same problem still.

Then, you may have to inspect the proof in the interactive GUI. Such memory exhaustion likely is due to looping, but this is no guarantee. 

I did not have the time to look into your code.

Best regards,
Ralf

--
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/5d988c96-6b94-44c5-a536-45ed64414c71n%40googlegroups.com.