Assignment deadline extension policies help students manage academic responsibilities alongside personal challenges. While increasingly used in higher education, these policies are especially relevant in computer engineering programs due to frequent and numerous assignments. Therefore, this study focused on a policy allowing students to use two one-day extensions without penalty, examining how computer engineering undergraduates (n=99) utilized them in relation to socio-demographic and academic factors. Our mixed-methods analysis using contingency table analyses and chi-squared tests found no significant associations between extension usage and gender, race, first-generation status, or employment as a critical dimension of diversity influencing academic experiences. However, a notable association emerged based on Cumulative Grade Point Averages (CGPA) groups, revealing that students with higher GPAs (3.5-4.0) were likelier to use both extensions than those with lower GPAs. These differences were primarily driven by variations between non-users and those who utilized both extensions. The qualitative findings showed common positive views of the policy for reducing stress and helping manage workloads during emergencies. While non-users raised concerns about potential overreliance on such extensions, users expressed frustration with the limited number of extensions in a semester and the short duration, which added to their stress. Thus, the findings underline the importance of designing extension policies that balance flexibility and fairness, addressing diverse student needs while encouraging responsible usage.

Runtime verificationis a technique, where amonitorprocess extracts information from a running system in order to evaluate whether system executions violate or satisfy a given correctness specification. In this paper, we consider runtime verification of synchronous distributed systems, where a set of decentralized monitors that only have a partial view of the system are subject tocrash failures. In this context, it is unavoidable that monitors may have different views of the underlying system, and, therefore, have different opinions about the correctness property. We propose an automata-based synchronous monitoring algorithm that copes with$t$crash monitor failures. In our proposed approach, local monitors do not communicate their explicit reading of the underlying system. Rather, they emit asymbolic verdictthat efficiently encodes their partial views. This significantly reduces the communication overhead. To this end, we also introduce an (offline) SMT-based monitor synthesis algorithm, which results in minimizing the size of monitoring messages. We evaluate our algorithm on a wide range of formulas and observe an average of 2.5 times increase in the number of states of the monitor automaton.

Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Verifying the runtime correctness of smart contracts is a problem of compelling practical interest since, smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties. Such verification is challenging since smart contract execution is time sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring MTL specifications which employs SMT solving techniques and report experimental results.

Blockchains present a secure and reliable ledger to store transactions, but ensuring that a set of transactions follow a certain policy is difficult. In this paper we present a runtime verification approach to monitor transactions involving multiple blockchains with respect to specifications in metric temporal logic (MTL). In our setting, we consider runtime verification of partially synchronous blockchains where a clock synchronization algorithm guarantees a bound on maximum clock skew among all the blockchains in the system.

In this paper, we study the problem of runtime verification of distributed applications that do not share a global clock with respect to specifications in the linear temporal logics (LTL). Our proposed method distinguishes from the existing work in three novel ways. First, we make a practical assumption that the distributed system under scrutiny is augmented with a clock synchronization algorithm that guarantees bounded clock skew among all processes. Second, we do not make any assumption about the structure of predicates that form LTL formulas. This relaxation allows us to monitor a wide range of applications that was not possible before. Subsequently, we propose a distributed monitoring algorithm by employing SMT solving techniques. Third, given the fact that distributed applications nowadays run on massive cloud services, we extend our solution to a parallel monitoring algorithm to utilize the available computing infrastructure. We report on rigorous synthetic as well as real-world case studies and demonstrate that scalable online monitoring of distributed applications is within our reach.