Concurrency bugs are notoriously hard to detect and reproduce. Controlled concurrency testing (CCT) techniques aim to offer a solution, where a scheduler explores the space of possible interleavings of a concurrent program looking for bugs. Since the set of possible interleavings is typically very large, these schedulers employ heuristics that prioritize the search to “interesting” subspaces. However, current heuristics are typically tuned to specific bug patterns, which limits their effectiveness in practice. In this paper, we present QL, a learning-based CCT framework where the likelihood of an action being selected by the scheduler is influenced by earlier explorations. We leverage the classical Q-learning algorithm to explore the space of possible interleavings, allowing the exploration to adapt to the program under test, unlike previous techniques. We have implemented and evaluated QL on a set of microbenchmarks, complex protocols, as well as production cloud services. In our experiments, we found QL to consistently outperform the state-of-the-art in CCT.

Background: As cardiovascular medicine advances rapidly, the integration of artificial intelligence (AI) has garnered increasing attention. Although AI has been widely adopted in diagnostics, risk prediction, and decision support, its application in exercise-based cardiovascular rehabilitation is still limited, representing a new and promising research frontier. Objective: This scoping review aimed to identify and analyze original studies that have applied AI to exercise-based interventions designed to improve cardiovascular outcomes. Methods: Following the PRISMA-ScR guidelines, PubMed, Scopus, Web of Science, Embase, and IEEE Xplore were searched for articles published between January 2015 and August 2025. Eligible studies were peer-reviewed by human research employing AI (machine learning or deep learning) to deliver, adapt, or monitor an exercise intervention with cardiovascular outcomes. Reviews, diagnostic-only studies, protocols without data, and animal studies were excluded. Non-original works (reviews, protocols), animal studies, and purely diagnostic applications were excluded, ensuring a strict focus on AI applied within exercise interventions. Data extraction focused on study design, AI method, exercise modality, outcomes, and findings. Results: From 2183 records, nine studies met the inclusion criteria (two RCTs, feasibility pilots, and validation studies). Designs included feasibility pilots, randomized controlled trials (RCTs), and validation studies. AI applications encompassed adaptive step goals, reinforcement learning for engagement, coaching apps, machine learning–based exercise prescription, and continuous monitoring (e.g., VO₂ estimation). These AI methods, such as machine learning and reinforcement learning, were used to personalize exercise interventions and improve cardiovascular outcomes. Reported outcomes included blood pressure reduction, improved adherence, increased daily steps, improvement in VO₂max, continuous physiological monitoring, and enhanced diagnostic accuracy. Conclusions: Findings demonstrate that AI has the potential to significantly enhance cardiovascular rehabilitation. It can personalize exercise prescriptions, enhance adherence, and facilitate safe monitoring in home settings. However, the evidence base remains preliminary, with very few RCTs and substantial methodological heterogeneity. Future research must prioritize large-scale clinical trials, explainable AI, and equitable implementation strategies to ensure clinical translation.

Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification.

Background: As cardiovascular medicine advances rapidly, the integration of artificial intelligence (AI) has garnered increasing attention. Despite its growing application across various domains, the role of AI in exercise-based interventions remains relatively underexplored, offering a novel and promising direction for future research. Objective: This scoping review aimed to identify and analyse original studies that have applied AI to exercise-based interventions designed to improve cardiovascular outcomes. Methods: Following the PRISMA-ScR guidelines, PubMed, Scopus, Web of Science, Embase, and IEEE Xplore were searched for articles published between January 2015 and August 2025. Eligible studies were peer-reviewed human research employing AI (machine learning or deep learning) to deliver, adapt, or monitor an exercise intervention with cardiovascular outcomes. Reviews, diagnostic-only studies, protocols without data, and animal studies were excluded. Data extraction focused on study design, AI method, exercise modality, outcomes, and findings. Results: From 2,183 records, 11 studies met the inclusion criteria. Designs included feasibility pilots, randomized controlled trials (RCTs), and validation studies. AI applications encompassed adaptive step goals, reinforcement learning for engagement, coaching apps, machine learning–based exercise prescription, and continuous monitoring (e.g., VO₂ estimation). These AI methods, such as machine learning and reinforcement learning, were used to personalize exercise interventions and improve cardiovascular outcomes. Reported outcomes included blood pressure reduction, improved adherence, increased daily steps, improvement in VO₂max, continuous physiological monitoring, and enhanced diagnostic accuracy. Conclusions: Although evidence remains limited, findings demonstrate AI’s potential to personal exercise interventions, enable continuous monitoring, and enhance adherence in cardiovascular care. These findings suggest that AI could be a valuable tool in the development of more effective and personalized exercise-based interventions. However, large-scale RCTs, methodological standardization, and explainable AI approaches are urgently needed to ensure reliability, equity, and clinical translation. These future research directions are crucial for the successful integration of AI in cardiovascular care.

This paper describes the design and implementation of the open-source tool $$\textsc {Coyote} $$ for testing concurrent programs written in the $$\textsc {C}{} \texttt {\#} $$ language. $$\textsc {Coyote} $$ provides algorithmic capabilities to explore the state-space of interleavings of a concurrent program, with deterministic repro for any bug that it finds. $$\textsc {Coyote} $$ encapsulates multiple ideas from the research community to offer state-of-the-art testing for $$\textsc {C}{} \texttt {\#} $$ programs, as well as an efficiently engineered implementation that has been shown robust enough to support industrial use.

Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. Using our framework, a programmer can build an application as several (possibly distributed) RSMs that communicate with each other via messages, much in the style of actor-based programming. Each RSM is additionally fault-tolerant by design and offers the illusion of being "always-alive". An RSM is guaranteed to process each input request exactly once, as one would expect in a failure-free environment. The RSM runtime automatically takes care of persisting state and rehydrating it on a failover. We present the core syntax and semantics of RSMs, along with a formal proof of failure-transparency. We provide an implementation of the RSM framework and runtime on the .NET platform for deploying services to Microsoft Azure. We carried out an extensive performance evaluation on micro-benchmarks to show that one can build high-throughput applications with RSMs. We also present a case study where we rewrote a significant part of a production cloud service using RSMs. The resulting service has simpler code and exhibits production-grade performance.