SS
S. Stoicescu
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
2 records found
1
Model-Guided Fuzzing for Apache Accord
Evaluating Predicate-Based Coverage as a Practical Alternative to TLA+
Master thesis
(2026)
-
S. Stoicescu, B. Özkan, E.B. Gülcan, Jérémie Decouchant, A. Katsifodimos, Alexey Gotsman, Benedict Elliott Smith
Distributed consensus protocols are the backbone of modern cloud infrastructure, ensuring consistency across replicated state machines. Leaderless consensus algorithms, such as Apache Accord, achieve optimal latency (1-RTT) by effectively distributing the ordering load across the cluster; however, this comes at the cost of significant algorithmic complexity during fault recovery. When a coordinating node crashes, surviving replicas must reconstruct dependency and ordering information by combining partial histories. A recent report by Ryabinin et al. demonstrates that non-trivial linearizability bugs can occur in Accord's recovery logic under very specific network and node failure conditions.
Finding such flaws through trace-guided fuzzing is infeasible because the number of message interleavings makes almost every execution appear distinct. We adapt ModelFuzz, which uses abstract TLA+ states as a coverage signal, by extending Accord's testing framework with controlled message delivery, crash injection, and a mapping from implementation executions to the formal model. We also introduce predicate coverage, a lighter-weight alternative derived from protocol stages, quorum progress, and crashed replicas. ModelFuzz achieves the highest TLA+ state coverage, while the most detailed predicate configuration can outperform unguided baselines but remains significantly behind ModelFuzz. Controlled exploration also exposes a reproducible internal correctness failure in Accord. ...
Finding such flaws through trace-guided fuzzing is infeasible because the number of message interleavings makes almost every execution appear distinct. We adapt ModelFuzz, which uses abstract TLA+ states as a coverage signal, by extending Accord's testing framework with controlled message delivery, crash injection, and a mapping from implementation executions to the formal model. We also introduce predicate coverage, a lighter-weight alternative derived from protocol stages, quorum progress, and crashed replicas. ModelFuzz achieves the highest TLA+ state coverage, while the most detailed predicate configuration can outperform unguided baselines but remains significantly behind ModelFuzz. Controlled exploration also exposes a reproducible internal correctness failure in Accord. ...
Distributed consensus protocols are the backbone of modern cloud infrastructure, ensuring consistency across replicated state machines. Leaderless consensus algorithms, such as Apache Accord, achieve optimal latency (1-RTT) by effectively distributing the ordering load across the cluster; however, this comes at the cost of significant algorithmic complexity during fault recovery. When a coordinating node crashes, surviving replicas must reconstruct dependency and ordering information by combining partial histories. A recent report by Ryabinin et al. demonstrates that non-trivial linearizability bugs can occur in Accord's recovery logic under very specific network and node failure conditions.
Finding such flaws through trace-guided fuzzing is infeasible because the number of message interleavings makes almost every execution appear distinct. We adapt ModelFuzz, which uses abstract TLA+ states as a coverage signal, by extending Accord's testing framework with controlled message delivery, crash injection, and a mapping from implementation executions to the formal model. We also introduce predicate coverage, a lighter-weight alternative derived from protocol stages, quorum progress, and crashed replicas. ModelFuzz achieves the highest TLA+ state coverage, while the most detailed predicate configuration can outperform unguided baselines but remains significantly behind ModelFuzz. Controlled exploration also exposes a reproducible internal correctness failure in Accord.
Finding such flaws through trace-guided fuzzing is infeasible because the number of message interleavings makes almost every execution appear distinct. We adapt ModelFuzz, which uses abstract TLA+ states as a coverage signal, by extending Accord's testing framework with controlled message delivery, crash injection, and a mapping from implementation executions to the formal model. We also introduce predicate coverage, a lighter-weight alternative derived from protocol stages, quorum progress, and crashed replicas. ModelFuzz achieves the highest TLA+ state coverage, while the most detailed predicate configuration can outperform unguided baselines but remains significantly behind ModelFuzz. Controlled exploration also exposes a reproducible internal correctness failure in Accord.
Predicting model deformations for predictive force feedback in haptic bilateral teleoperation applications
Towards complex interactions in haptic bilateral teleoperation
In this paper, we investigate the use of heightmap-based models to predict deformations in granular materials during teleoperation tasks. Our primary objective is to provide real-time cutting feedback and contact predictions for haptic bilateral teleoperation applications, thereby enhancing operator control in remote manipulation scenarios. We developed a simulation model that utilizes heightmaps to represent deformable materials and implemented a cutting algorithm to simulate complex interactions with granular soils.
Through a series of experiments, we demonstrated that higher resolution heightmaps significantly improve the accuracy and stability of cutting feedback. Our findings suggest that this approach is a viable method for keeping track of changes in a deformable object's shape and can be further expanded to include a wider range of teleoperation tasks, potentially improving the safety and effectiveness of remote operations in hazardous environments. ...
Through a series of experiments, we demonstrated that higher resolution heightmaps significantly improve the accuracy and stability of cutting feedback. Our findings suggest that this approach is a viable method for keeping track of changes in a deformable object's shape and can be further expanded to include a wider range of teleoperation tasks, potentially improving the safety and effectiveness of remote operations in hazardous environments. ...
In this paper, we investigate the use of heightmap-based models to predict deformations in granular materials during teleoperation tasks. Our primary objective is to provide real-time cutting feedback and contact predictions for haptic bilateral teleoperation applications, thereby enhancing operator control in remote manipulation scenarios. We developed a simulation model that utilizes heightmaps to represent deformable materials and implemented a cutting algorithm to simulate complex interactions with granular soils.
Through a series of experiments, we demonstrated that higher resolution heightmaps significantly improve the accuracy and stability of cutting feedback. Our findings suggest that this approach is a viable method for keeping track of changes in a deformable object's shape and can be further expanded to include a wider range of teleoperation tasks, potentially improving the safety and effectiveness of remote operations in hazardous environments.
Through a series of experiments, we demonstrated that higher resolution heightmaps significantly improve the accuracy and stability of cutting feedback. Our findings suggest that this approach is a viable method for keeping track of changes in a deformable object's shape and can be further expanded to include a wider range of teleoperation tasks, potentially improving the safety and effectiveness of remote operations in hazardous environments.