monabs swMATH ID: 18507 Software Authors: Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas Description: Lost in abstraction: monotonicity in multi-threaded programs. Monotonicity in concurrent systems stipulates that, in any global state, system actions remain executable when new processes are added to the state. This concept is both natural and useful: if every thread’s memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unknown. In this paper, we show that finite-data thread abstractions for model checking can be at odds with monotonicity: predicate-abstracting monotone software can result in non-monotone Boolean programs – the monotonicity is {it lost in the abstraction}. As a result, pertinent well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity in the abstraction can be restored, without affecting safety properties. This improves earlier approaches of enforcing monotonicity via overapproximations. We implemented our solution in the unbounded-thread model checker \(mathsf{monabs}\) and applied it to numerous concurrent programs and algorithms, whose predicate abstractions are often fundamentally beyond existing tools. Homepage: http://www.sciencedirect.com/science/article/pii/S0890540116000407 Keywords: multi-threaded software; parameterized verification; monotonicity; predicate abstraction Related Software: ACL2s; veriSoft; DDVerify; MAGIC; Threader; SLAB; SymmPa; SAS Cited in: 3 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Lost in abstraction: monotonicity in multi-threaded programs. Zbl 1355.68055Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas 2017 Cited by 4 Authors 3 Wahl, Thomas 2 Kaiser, Alexander D. 2 Kröning, Daniel 1 Johnson, Andrew D. Cited in 1 Serial 1 Information and Computation Cited in 1 Field 3 Computer science (68-XX) Citations by Year