Dear sanjanasai,
thank you for your interest in CPAchecker!
Am 11.12.23 um 14:10 schrieb sanjanasai:
> I am working on verification of multithreaded applications based on C code
> and focusing on the detection of the deadlock and race conditions in the
> multithreaded C applications which was backed by your paper "A Light-Weight
> Approach for Verifying Multi-Threaded
> Programs with CPAchecker" , the snippet referring to especially the
> deadlock detection as attached. Based on the statement, I could not find a
> command or instructions directly pertaining to the deadlock detection in
> the tool manual.
The observer automaton that is referred to in the paper is in file
"config/specification/deadlock.spc" in the CPAchecker repository.
The best suited deadlock analysis should be
config/deadlock-detection.properties AFAIK, so you will have the best
chance with the following parameters:
-deadlock-detection -spec deadlock
However, please note that the respective parts of CPAchecker are not
under active development currently and not all people involved in that
project are active anymore.
So it may be that you encounter some open issues.
Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181