Eliminating Message Counters in Synchronous Threshold Automata
In previous work, we introduced synchronous threshold automata for the verification of synchronous fault-tolerant distributed algorithms, and presented a verification method based on bounded model checking. Modeling a distributed algorithm by a threshold automaton requires to correctly deal with the semantics for sending and receiving messages based on the fault assumption. This step was done manually so far, and required human ingenuity. Motivated by similar results for asynchronous threshold automata, in this paper we show that one can start from a faithful model of the distributed algorithm that includes the sending and receiving of messages, and then automatically obtain a threshold automaton by applying quantifier elimination on the receive message counters. In this way, we obtain a fully automated verification pipeline. We present an experimental evaluation, discovering a bug in our previous manual encoding. Interestingly, while quantifier elimination in general produces larger threshold automata than the manual encoding, the verification times are comparable and even faster in several cases, allowing us to verify benchmarks that could not be handled before.
Sun 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:30: Concurrent and Distributed SystemsVMCAI at VMCAI Chair(s): Dana Drachsler CohenTechnion | |||
18:30 - 18:45 Talk | Concurrent Correctness in Vector Space VMCAI Christina PetersonUniversity of Central Florida, Victor CookUniversity of Central Florida, Damian DechevUniversity of Central Florida Media Attached | ||
18:45 - 19:00 Talk | Verification of Concurrent Programs Using Petri Net Unfoldings VMCAI Daniel DietschUniversity of Freiburg, Matthias HeizmannUniversity of Freiburg, Germany, Dominik KlumppUniversity of Freiburg, Mehdi NaouarUniversity of Freiburg, Andreas PodelskiUniversity of Freiburg, Germany, Claus SchätzleUniversity of Freiburg Media Attached | ||
19:00 - 19:15 Talk | Eliminating Message Counters in Synchronous Threshold Automata VMCAI Ilina StoilkovskaVienna University of Technology , Igor KonnovInformal Systems Inc, Josef WidderInformal Systems, Florian ZulegerVienna University of Technology Media Attached | ||
19:15 - 19:30 Talk | A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries VMCAI Nathalie BertrandINRIA Rennes, Marijana LazicTechnical University of Munich, Josef WidderInformal Systems Media Attached |