27 citations · 35 across the 6 of their papers we have counts for
6 papers
Decidability of Liveness on the TSO Memory Model
Chao Wang, Gustavo Petri, Yi Lv +2
An important property of concurrent objects is whether they support progress -a special case of liveness-guarantees, which ensure the termination of individual method calls under s…
Replication-Aware Linearizability
Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri +1
Geo-distributed systems often replicate data at multiple locations to achieve availability and performance despite network partitions. These systems must accept updates at any repl…
Flow-Sensitive Composition of Thread-Modular Abstract Interpretation
Markus Kusano, Chao Wang
We propose a constraint-based flow-sensitive static analysis for concurrent programs by iteratively composing thread-modular abstract interpreters via the use of a system of lightw…
Modular Verification of Interrupt-Driven Software
Chungha Sung, Markus Kusano, Chao Wang
Interrupts have been widely used in safety-critical computer systems to handle outside stimuli and interact with the hardware, but reasoning about interrupt-driven software remains…
Thread-Modular Static Analysis for Relaxed Memory Models
Markus Kusano, Chao Wang
We propose a memory-model-aware static program analysis method for accurately analyzing the behavior of concurrent software running on processors with weak consistency models such…
Shield Synthesis: Runtime Enforcement for Reactive Systems
Roderick Bloem, Bettina Koenighofer, Robert Koenighofer +1
Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a "safety shield" that is attached…