The 2016 Clinical TempEval continued the 2015 shared task on temporal information extraction with a new evaluation test set. Our team, UtahBMI, participated in all subtasks using machine learning approaches with ClearTK (LIBLINEAR), CRF++ and CRFsuite packages. Our experiments show that CRF-based classifiers yield, in general, higher recall for multi-word spans, while SVM-based classifiers are better at predicting correct attributes of TIMEX3. In addition, we show that an ensemble-based approach for TIMEX3 could yield improved results. Our team achieved competitive results in each subtask with an F1 75.4% for TIMEX3, F1 89.2% for EVENT, F1 84.4% for event relations with document time (DocTimeRel), and F1 51.1% for narrative container (CONTAINS) relations.

In the online sorting problem, n items are revealed one by one and have to be placed (immediately and irrevocably) into empty cells of a size-n array. The goal is to minimize the sum of absolute differences between items in consecutive cells. This natural problem was recently introduced by Aamand, Abrahamsen, Beretta, and Kleist (SODA 2023) as a tool in their study of online geometric packing problems. They showed that when the items are reals from the interval [0, 1] a competitive ratio of O(√n) is achievable, and no deterministic algorithm can improve this ratio asymptotically. In this paper, we extend and generalize the study of online sorting in three directions: randomized: we settle the open question of Aamand et al. by showing that the O(√n) competitive ratio for the online sorting of reals cannot be improved even with the use of randomness; stochastic: we consider inputs consisting of n samples drawn uniformly at random from an interval, and give an algorithm with an improved competitive ratio of Oe(n1/4). The result reveals connections between online sorting and the design of efficient hash tables; high-dimensional: we show that Oe(√n)-competitive online sorting is possible even for items from Rd, for arbitrary fixed d, in an adversarial model. This can be viewed as an online variant of the classical TSP problem where tasks (cities to visit) are revealed one by one and the salesperson assigns each task (immediately and irrevocably) to its timeslot. Along the way, we also show a tight O(log n)-competitiveness result for uniform metrics, i.e., where items are of different types and the goal is to order them so as to minimize the number of switches between consecutive items of different types.

We devise a polynomial-time algorithm for partitioning a simple polygon P into a minimum number of star-shaped polygons. The question of whether such an algorithm exists has been open for more than four decades [Avis and Toussaint, Pattern Recognit., 1981] and it has been repeated frequently, for example in O'Rourke's famous book [Art Gallery Theorems and Algorithms, 1987]. In addition to its strong theoretical motivation, the problem is also motivated by practical domains such as CNC pocket milling, motion planning, and shape parameterization. The only previously known algorithm for a non-trivial special case is for P being both monotone and rectilinear [Liu and Ntafos, Algorithmica, 1991]. For general polygons, an algorithm was only known for the restricted version in which Steiner points are disallowed [Keil, SIAM J. Comput., 1985], meaning that each corner of a piece in the partition must also be a corner of P. Interestingly, the solution size for the restricted version may be linear for instances where the unrestricted solution has constant size. The covering variant in which the pieces are star-shaped but allowed to overlap - known as the Art Gallery Problem - was recently shown to be ∃ℝ-complete and is thus likely not in NP [Abrahamsen, Adamaszek and Miltzow, STOC 2018 & J. ACM 2022]; this is in stark contrast to our result. Arguably the most related work to ours is the polynomial-time algorithm to partition a simple polygon into a minimum number of convex pieces by Chazelle and Dobkin [STOC, 1979 & Comp. Geom., 1985].

This work initiates the study of property testing in signed graphs, where every edge has either a positive or a negative sign. We show that there exist sublinear query and time algorithms for testing three key properties of signed graphs: balance (or 2-clusterability), clusterability and signed triangle freeness. We consider both the dense graph model, where one queries the adjacency matrix entries of a signed graph, and the bounded-degree model, where one queries for the neighbors of a node and the sign of the connecting edge. Our algorithms use a variety of tools from unsigned graph property testing, as well as reductions from one setting to the other. Our main technical contribution is a sublinear algorithm for testing clusterability in the bounded-degree model. This contrasts with the property of k-clusterability in unsigned graphs, which is not testable with a sublinear number of queries in the bounded-degree model. We experimentally evaluate the complexity and usefulness of several of our testers on real-life and synthetic datasets.

We consider the problem of adding a fixed number of new edges to an undirected graph in order to minimize the diameter of the augmented graph, and under the constraint that the number of edges added for each vertex is bounded by an integer. The problem is motivated by network-design applications, where we want to minimize the worst case communication in the network without excessively increasing the degree of any single vertex, so as to avoid additional overload. We present three algorithms for this task, each with their own merits. The special case of a matching augmentation -when every vertex can be incident to at most one new edge- is of particular interest, for which we show an inapproximability result, and provide bounds on the smallest achievable diameter when these edges are added to a path. Finally, we empirically evaluate and compare our algorithms on several real-life networks of varying types.

An important challenge in the field of exponential random graphs (ERGs) is the fitting of non-trivial ERGs on large graphs. By utilizing fast matrix block-approximation techniques, we propose an approximative framework to such non-trivial ERGs that result in dyadic independence (i.e., edge independent) distributions, while being able to meaningfully model local information of the graph (e.g., degrees) as well as global information (e.g., clustering coefficient, assortativity, etc.) if desired. This allows one to efficiently generate random networks with similar properties as an observed network, and the models can be used for several downstream tasks such as link prediction. Our methods are scalable to sparse graphs consisting of millions of nodes.Empirical evaluation demonstrates competitiveness in terms of both speed and accuracy with state-of-the-art methods - which are typically based on embedding the graph into some low-dimensional space - for link prediction, showcasing the potential of a more direct and interpretable probablistic model for this task.

Structural bias or segregation of networks refers to situations where two or more disparate groups are present in the network, so that the groups are highly connected internally, but loosely connected to each other. Examples include polarized communities in social networks, antagonistic content in video-sharing or news-feed platforms, etc. In many cases it is of interest to increase the connectivity of disparate groups so as to, e.g., minimize social friction, or expose individuals to diverse viewpoints. A commonly-used mechanism for increasing the network connectivity is to add edge shortcuts between pairs of nodes. In many applications of interest, edge shortcuts typically translate to recommendations, e.g., what video to watch, or what news article to read next. The problem of reducing structural bias or segregation via edge shortcuts has recently been studied in the literature, and random walks have been an essential tool for modeling navigation and connectivity in the underlying networks. Existing methods, however, either do not offer approximation guarantees, or engineer the objective so that it satisfies certain desirable properties that simplify the optimization task. In this paper we address the problem of adding a given number of shortcut edges in the network so as to directly minimize the average hitting time and the maximum hitting time between two disparate groups. The objectives we study are more natural than objectives considered earlier in the literature (e.g., maximizing hitting-time reduction) and the optimization task is significantly more challenging. Our algorithm for minimizing average hitting time is a greedy bicriteria that relies on supermodularity. In contrast, maximum hitting time is not supermodular. Despite, we develop an approximation algorithm for that objective as well, by leveraging connections with average hitting time and the asymmetric k-center problem.

Smart home devices collect and transmit user data to smart home Trigger Action Platforms (TAPs) for processing and executing automation rules. However, this data can also be used to infer user activities or other sensitive information. In this paper, we propose PTAP, a privacy-preserving approach based on adversarial example attacks. PTAP injects targeted perturbations into time-series sensor data, effectively confounding potentially malicious TAP classifiers. Our approach significantly reduces the chance of user activity recognition for a malicious TAP while preserving the essential information for automation rule execution, thus safeguarding TAP utility. We evaluated PTAP using a real-world smart-home dataset and examined its effectiveness in preserving utility through the execution of various IoT applications. Our results demonstrate that PTAP effectively preserves user privacy (reducing the accuracy of a malicious classifier 91 to 6 percent) while maintaining automation rule integrity, providing a practical and effective solution to protect user privacy in smart-home environments.

Information flow control and dynamic policies is a difficult relationship yet to be fully understood. While dynamic policies are a natural choice in many real-world applications that downgrade and upgrade the sensitivity of information, understanding the meaning of security in this setting is challenging. In this paper we revisit the knowledge-based security conditions to reinstate a simple and intuitive security condition for dynamic policies: A program is secure if at any point during the execution the attacker's knowledge is in accordance with the active security policy at that execution point. Our key observation is the new notion of policy consistency to prevent policy changes whenever an attacker is already in possession of the information that the new policy intends to protect. We use this notion to study a range of realistic attackers including the perfect recall attacker, bounded attackers, and forgetful attackers, and their relationship. Importantly, our new security condition provides a clean connection between the dynamic policy and the underlying attacker model independently of the specific use case. We illustrate this by considering the different facets of dynamic policies in our framework. On the verification side, we design and implement DynCoVer, a tool for checking dynamic information-flow policies for Java programs via symbolic execution and SMT solving. Our verification operates by first extracting a graph of program dependencies and then visiting the graph to check dynamic policies for a range of attackers. We evaluate the effectiveness and efficiency of DyncoVeron a benchmark of use cases from the literature and designed by ourselves, as well as the case study of a social network. The results show that DynCoVer can analyze small but intricate programs indicating that it can help verify security-critical parts of Java applications. We release Dyncover publicly to support open science and encourage researchers to explore the topic further.

When specifying security policies for databases, it is often natural to formulate disjunctive dependencies, where a piece of information may depend on at most one of two dependencies P-1 or P-2, but not both. A formal semantic model of such disjunctive dependencies, the Quantale of Information, was recently introduced by Hunt and Sands as a generalization of the Lattice of Information. In this paper, we seek to contribute to the understanding of disjunctive dependencies in database-backed programs and introduce a practical framework to statically enforce disjunctive security policies. To that end, we introduce the Determinacy Quantale, a new query-based structure which captures the ordering of disjunctive information in databases. This structure can be understood as a query-based counterpart to the Quantale of Information. Based on this structure, we design a sound enforcement mechanism to check disjunctive policies for database-backed programs. This mechanism is based on a type-based analysis for a simple imperative language with database queries, which is precise enough to accommodate a variety of row- and column-level database policies flexibly while keeping track of disjunctions due to control flow. We validate our mechanism by implementing it in a tool, DIVERT, and demonstrate its feasibility on a number of use cases.

Trigger-Action Platforms (TAPs) play a vital role in fulfilling the promise of the Internet of Things (IoT) by seamlessly connecting otherwise unconnected devices and services. While enabling novel and exciting applications across a variety of services, security and privacy issues must be taken into consideration because TAPs essentially act as persons-in-the-middle between trigger and action services. The issue is further aggravated since the triggers and actions on TAPs are mostly provided by third parties extending the trust beyond the platform providers. Node-RED, an open-source JavaScript-driven TAP, provides the opportunity for users to effortlessly employ and link nodes via a graphical user interface. Being built upon Node.js, third-party developers can extend the platform’s functionality through publishing nodes and their wirings, known as flows. This paper proposes an essential model for Node-RED, suitable to reason about nodes and flows, be they benign, vulnerable, or malicious. We expand on attacks discovered in recent work, ranging from exfiltrating data from unsuspecting users to taking over the entire platform by misusing sensitive APIs within nodes. We present a formalization of a runtime monitoring framework for a core language that soundly and transparently enforces fine-grained allowlist policies at module-, API-, value-, and context-level. We introduce the monitoring framework for Node-RED that isolates nodes while permitting them to communicate via well-defined API calls complying with the policy specified for each node.

Trigger-Action Platforms (TAPs) seamlessly connect a wide variety of otherwise unconnected devices and services, ranging from IoT devices to cloud services and social networks. TAPs raise critical security and privacy concerns because a TAP is effectively a "person-in-the-middle" between trigger and action services. Third-party code, routinely deployed as "apps" on TAPs, further exacerbates these concerns. This paper focuses on JavaScript-driven TAPs. We show that the popular IFTTT and Zapier platforms and an open-source alternative Node-RED are susceptible to attacks ranging from exfiltrating data from unsuspecting users to taking over the entire platform. We report on the changes by the platforms in response to our findings and present an empirical study to assess the implications for Node-RED. Motivated by the need for a secure yet flexible way to integrate third-party JavaScript apps, we propose SandTrap, a novel JavaScript monitor that securely combines the Node.js vm module with fully structural proxy-based two-sided membranes to enforce fine-grained access control policies. To aid developers, SandTrap includes a policy generation mechanism. We instantiate SandTrap to IFTTT, Zapier, and Node-RED and illustrate on a set of benchmarks how SandTrap enforces a variety of policies while incurring a tolerable runtime overhead.

This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.

Automated Human Activity Recognition (HAR) stems from the requirement to seamlessly integrate technology into daily life, to enhance user experience, improve healthcare, provide improved operations, ensure safety, deliver data-driven insights, and address various real-world challenges. However, unscripted Human activity faces challenges that must be understood, and require advances in sensor technology and machine learning models. This paper presents an Active Transfer Learning (ATL) approach for real-time HAR using mobile sensor data. Unlike traditional methods, our approach accounts for both the physical and habitual constraints of individuals. Existing works make an unrealistic assumption of an omniscient oracle while using the same datasets for both training and testing of the models, which makes them impractical for industry requirements. Our proposed approach addresses challenges in existing HAR algorithms, proposing a methodology to adapt models to the real-world datasets while training and testing on cross datasets. We have tailored an existing Entropy and Memory Maximization algorithm to work in a real-time environment while considering user constraints. Primarily trained in a well-labeled controlled environment dataset, we introduce noise injection to prevent the model from overfitting and enhance its generalization for scarcely labeled real-world datasets. Evaluations on publicly available datasets demonstrate our approach achieves 80% - 90% accuracy, outperforming the base algorithm accuracy of 12% - 14%. Importantly, our proposed technique outperforms with limited labeled data, making it valuable for real-time scenarios where labeling is sparse. This research advances HAR in real-world settings, offering improved accuracy and adaptability.

Assertion-based software model checking refers to techniques that take a program annotated with logical assertions and statically verify that the assertions hold whenever program execution is at the corresponding control point. While the associated annotation overhead is relatively low, these techniques are typically monolithic in that they explore the state space of the whole program at once, and may therefore scale poorly to large programs. Deductive software verification, on the other hand, refers to techniques that prove the correctness of a piece of software against a detailed specification of what it is supposed to accomplish or compute. The associated verification techniques are modular and scale well to large code bases, but incur an annotation overhead that is often very high, which is a real obstacle for deductive verification to be adopted in industry on a wider scale. In this paper we explore synergies between the two mentioned paradigms, and in particular, investigate how interpolation-based Horn solvers used for software model checking can be instrumented to infer missing procedure contracts for use in deductive verification, thus aiding the programmer in the code annotation process. We summarise the main developments in the area of automated contract inference, and present our own experiments with contract inference for C programs, based on solving Horn clauses. To drive the inference process, we put program assertions in the main function, and adapt our TriCera tool, a model checker based on the Horn solver Eldarica, to infer candidate contracts for all other functions. The contracts are output in the ANSI C Specification Language (ACSL) format, and are then validated with the Frama-C deductive verification tool for C programs.

We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P416, the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4's lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.

We introduce a formal semantics of P4 for the HOL4 interactive theorem prover. We exploit properties of the language, like the absence of call by reference and the copy-in/copy-out mechanism, to define a heapless small-step semantics that is abstract enough to simplify verification, but that covers the main aspects of the language: interaction with the architecture via externs, table match, and parsers. Our formalization is written in the Ott metalanguage, which allows us to export definitions to multiple interactive theorem provers. The exported HOL4 semantics allows us to establish machine-checkable proofs regarding the semantics, properties of P4 programs, and soundness of analysis tools.

The Algorand blockchain is a secure and decentralized public ledger based on pure proof of stake rather than proof of work. At its core it is a novel consensus protocol with exactly one block certified in each round: that is, the protocol guarantees that the blockchain does not fork. In this paper, we report on our effort to model and formally verify the Algorand consensus protocol in the Coq proof assistant. Similar to previous consensus protocol verification efforts, we model the protocol as a state transition system and reason over reachable global states. However, in contrast to previous work, our model explicitly incorporates timing issues (e.g., timeouts and network delays) and adversarial actions, reflecting a more realistic environment faced by a public blockchain.

In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of flow graphs, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in C.

The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.

The problem of inconsistent planning in decision making, which leads to undesirable effects such as procrastination, has been studied in the behavioral-economics literature, and more recently in the context of computational behavioral models. Individuals, however, do not function in isolation, and successful projects most often rely on team work. Team performance does not depend only on the skills of the individual team members, but also on other collective factors, such as team spirit and cohesion. It is not an uncommon situation (for instance, experienced by the authors while working on this paper) that a hard-working individual has the capacity to give a good example to her team-mates and motivate them to work harder. In this paper we adopt the model of Kleinberg and Oren (EC'14) on time-inconsistent planning, and extend it to account for the influence of procrastination within the members of a team. Our first contribution is to model collaborative work so that the relative progress of the team members, with respect to their respective subtasks, motivates (or discourages) them to work harder. We compare the total cost of completing a team project when the team members communicate with each other about their progress, with the corresponding cost when they work in isolation. Our main result is a tight bound on the ratio of these two costs, under mild assumptions. We also show that communication can either increase or decrease the total cost. We also consider the problem of assigning subtasks to team members, with the objective of minimizing the negative effects of collaborative procrastination. We show that whereas a simple problem of forming teams of two members can be solved in polynomial time, the problem of assigning n tasks to n agents is NP-hard.

Admission of applicants to higher education in a fair, reliable, transparent, and efficient way is a real challenge, especially if there are more eligible applicants than available places and if there are applicants from many different educational systems. Previous research on best practices for admission to master’s programmes identified the key question about an applicant’s potential for success in studies, but was not able to provide an answer about how to rate the merits of the applicants. In this study, indicators for study success are analysed by comparing the study performance of 228 students in master’s programmes with their merits at the time of admission. The null hypothesis was that the applicant’s average grade at the time of admission is the only indictor for study success. After testing for potential bias using almost 20 possible other indicators, the null hypothesis had to be rejected for four indicators (in order of importance): (i) university ranking, (ii) length of bachelor’s studies within subject, (iii) English language test and (iv) subject matching between bachelor’s and master’s education. Evaluation of quality of prior education is tricky and results from this study clearly indicate that students from higher ranked universities possess better knowledge and stronger skills for our master’s programmes. Work is ongoing to improve the merit rating model by involving more master’s programmes at KTH and analysing performance data from a larger number of students.

The COVID-19 pandemic has accelerated the digitalization of the Swedish public sector, and to ensure the success of this ongoing process cybersecurity plays an integral part. While Sweden has come far in digitalization, the maturity of cybersecurity work across entities covers a wide range. One way of improving cybersecurity is through communication, thereby enhancing employee cyber situation awareness. In this paper, we conduct a census of Swedish public sector employee communication on cybersecurity at the beginning of the COVID-19 pandemic using questionnaires. The study shows that public sector entities find the same sources of information useful for their cybersecurity work. We find that nearly two thirds of administrative authorities and almost three quarters of municipalities are not yet at the implemented cybersecurity level. We also find that 71 % of municipalities have less than one dedicated staff for cybersecurity.

In recent years, the Swedish public sector has undergone rapid digitalization, while cybersecurity efforts have not kept even steps. This study investigates conditions for cybersecurity work at Swedish administrative authorities by examining organizational conditions at the authorities, what cybersecurity staff do to acquire the cyber situation awareness required for their role, as well as what experience cybersecurity staff have with incidents. In this study, 17 semi-structured interviews were held with respondents from Swedish administrative authorities. The results showed the diverse conditions for cybersecurity work that exist at the authorities and that a variety of roles are involved in that work. It was found that national-level support for cybersecurity was perceived as somewhat lacking. There were also challenges in getting access to information elements required for sufficient cyber situation awareness.

The exponential increase in the availability of large-scale mobility data has fueled the vision of smart cities that will transform our lives. The truth is that we have just scratched the surface of the research challenges that should be tackled in order to make this vision a reality. Consequently, there is an increasing interest among different research communities (ranging from civil engineering to computer science) and industrial stakeholders in building knowledge discovery pipelines over such data sources. At the same time, this widespread data availability also raises privacy issues that must be considered by both industrial and academic stakeholders. In this paper, we provide a wide perspective on the role that big data have in reshaping cities. The paper covers the main aspects of urban data analytics, focusing on privacy issues, algorithms, applications and services, and georeferenced data from social media. In discussing these aspects, we leverage, as concrete examples and case studies of urban data science tools, the results obtained in the “City of Citizens” thematic area of the Horizon 2020 SoBigData initiative, which includes a virtual research environment with mobility datasets and urban analytics methods developed by several institutions around Europe. We conclude the paper outlining the main research challenges that urban data science has yet to address in order to help make the smart city vision a reality.

We study the complexity of determining the edge connectivity of a simple graph with cut queries. We show that (i) there is a bounded-error randomized algorithm that computes edge connectivity with O(n) cut queries, and (ii) there is a bounded-error quantum algorithm that computes edge connectivity with (O) over tilde(root n) cut queries. To prove these results we introduce a new technique, called star contraction, to randomly contract edges of a graph while preserving non-trivial minimum cuts. In star contraction vertices randomly contract an edge incident on a small set of randomly chosen "center" vertices. In contrast to the related 2-out contraction technique of Ghaffari, Nowicki, and Thorup [SODA'20], star contraction only contracts vertex-disjoint star subgraphs, which allows it to be efficiently implemented via cut queries. The O(n) bound from item (i) was not known even for the simpler problem of connectivity, and it improves the O(n log(3) n) upper bound by Rubinstein, Schramm, and Weinberg [ITCS'18]. The bound is tight under the reasonable conjecture that the randomized communication complexity of connectivity is Omega(n log n), an open question since the seminal work of Babai, Frankl, and Simon [FOCS'86]. The bound also excludes using edge connectivity on simple graphs to prove a superlinear randomized query lower bound for minimizing a symmetric submodular function. The quantum algorithm from item (ii) gives a nearlyquadratic separation with the randomized complexity, and addresses an open question of Lee, Santha, and Zhang [SODA'21]. The algorithm can alternatively be viewed as computing the edge connectivity of a simple graph with (O) over tilde(root n) matrix-vector multiplication queries to its adjacency matrix. Finally, we demonstrate the use of star contraction outside of the cut query setting by designing a one-pass semi-streaming algorithm for computing edge connectivity in the complete vertex arrival setting. This contrasts with the edge arrival setting where two passes are required.

Simulator training is becoming increasingly important for training of time-critical and dynamic situations. Hence, how simulator training in such domains is planned, carried out and followed up becomes important. Based on a model prescribing such crucial aspects, ten decision-making training simulator facilities have been analyzed from an activity theoretical perspective. The analysis reveals several conflicts that exist between the training that is carried out and the defined training objectives. Although limitations in technology and organization are often alleviated by proficient instructors, it is concluded that there is a need for a structured approach to the design of training to be able to define the competencies and skills that ought to be trained along with relevant measurable training goals. Further, there is a need for a pedagogical model that takes the specifics of simulator training into account. Such a pedagogical model is needed to be able to evaluate the training, and would make it possible to share experiences and make comparisons between facilities in a structured manner.

In this paper, we extend work on model‐based testing for Apache ZooKeeper, to handle watchers (triggers) and improve scalability. In a distributed asynchronous shared storage like ZooKeeper, watchers deliver notifications on state changes. They are difficult to test because watcher notifications involve an initial action that sets the watcher, followed by another action that changes the previously seen state.

We show how to generate test cases for concurrent client sessions executing against ZooKeeper with the tool Modbat. The tests are verified against an oracle that takes into account all possible timings of network communication. The oracle has to verify that there exists a chain of events that triggers both the initial callback and the subsequent watcher notification. We show in detail how the oracle computes whether watch triggers are correct and how the model was adapted and improved to handle these features. Together with a new search improvement that increases both speed and accuracy, we are able to verify large test setups and confirm several defects with our model.

To evaluate software testing and program analysis tools, the research community relies on collections of sample programs (benchmarks) containing realistic code examples with defects. We investigated 23 benchmark projects for test generation in common programming languages and looked at how they can be categorized according to attributes such as programming language, number of programs and defects, license, and size. From our studies, it is evident that the development and especially maintenance of benchmarks are a big challenge. Out of the 23 benchmark projects we investigated, only four are still active as of today, and only nine have been updated after their initial release. With the underlying programming languages and platforms constantly evolving (often without full backward compatibility), this creates a challenge when comparing new tools to older ones. To exacerbate the situation, many benchmarks do not fully track the provenance and license of the code they include. Sustainable benchmark collections share these key factors: Open hosting of complete (actual) data allowing community involvement, systematic maintenance of license and authorship data, and a unified machine-readable format for such data.

Analyzing executions of concurrent software is very difficult Even if a trace is available, such traces are very hard to read and interpret. A textual trace contains a lot of data, most of which is not relevant to the issue at hand. Past visualization attempts either do not show concurrent behavior, or result in a view that is overwhelming for the user. We provide a visual analytics tool, VA4JVM, for error traces produced by either the Java Virtual Machine, or by Java Pathfinder. Its key features are a layout that spatially associates events with threads, a zoom function, and the ability to filter event data in various ways. We show in examples how filtering and zooming in can highlight a problem without having to read lengthy textual data.

We give an account of JPF’s current architecture as it has evolved over the last 20 years. Key changes include a modular, extensible design, and Java 11 support. Java 11 brought with it fundamental changes in the language and its runtime, in particular, a new modular library system, different compilation of string expressions to bootstrap methods, and changes in many internal interfaces that allow access to the loaded code and the virtual machine state. These changes required numerous adaptations in JPF to ensure a successful compilation and correct behavior under Java 11.

Testing networked systems is challenging. The client or server side cannot be tested by itself. We present a solution using tool "Modbat" that generates test cases for Java's network library java.nio, where we test both blocking and non-blocking network functions. Our test model can dynamically simulate actions in multiple worker and client threads, thanks to a carefully orchestrated design that covers non-determinism while ensuring progress.

This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

With the growing popularity of unmanned aerial vehicles (UAVs) for consumer applications, the number of accidents involving UAVs is also increasing rapidly. Therefore, motion safety of UAVs has become a prime concern for UAV operators. For a swarm of UAVs, a safe operation cannot be guaranteed without preventing the UAVs from colliding with one another and with static and dynamically appearing, moving obstacles in the flying zone. In this paper, we present an online, collision-free path generation and navigation system for swarms of UAVs. The proposed system uses geographical locations of the UAVs and of the successfully detected, static, and moving obstacles to predict and avoid the following: (1) UAV-to-UAV collisions, (2) UAV-to-static-obstacle collisions, and (3) UAV-to-moving-obstacle collisions. Our collision prediction approach leverages efficient runtime monitoring and complex event processing (CEP) to make timely predictions. A distinctive feature of the proposed system is its ability to foresee potential collisions and proactively find best ways to avoid predicted collisions in order to ensure safety of the entire swarm. We also present a simulation-based implementation of the proposed system along with an experimental evaluation involving a series of experiments and compare our results with the results of four existing approaches. The results show that the proposed system successfully predicts and avoids all three kinds of collisions in an online manner. Moreover, it generates safe and efficient UAV routes, efficiently scales to large-sized problem instances, and is suitable for cluttered flying zones and for scenarios involving high risks of UAV collisions.

Unmanned Aerial Vehicles (UAV) are a potential solution to fast and cost efficient package delivery services. There are two types of UAVs, namely fixed wing (UAV-FW) and rotor wing (UAV-RW), which have their own advantages and drawbacks. In this paper we aim at providing different solutions to a collaborating multi-agent scenario combining both UAVs types. We show the problem can be reduced to the facility location problem (FLP) and propose two local search algorithms to solve it: Tabu search and simulated annealing.

Bayesian networks are general, well-studied probabilistic models that capture dependencies among a set of variables. Variable Elimination is a fundamental algorithm for probabilistic inference over Bayesian networks. In this paper, we propose a novel materialization method, which can lead to significant efficiency gains when processing inference queries using the Variable Elimination algorithm. In particular, we address the problem of choosing a set of intermediate results to precompute and materialize, so as to maximize the expected efficiency gain over a given query workload. For the problem we consider, we provide an optimal polynomial-time algorithm and discuss alternative methods. We validate our technique using real-world Bayesian networks. Our experimental results confirm that a modest amount of materialization can lead to significant improvements in the running time of queries, with an average gain of 70%, and reaching up to a gain of 99%, for a uniform workload of queries. Moreover, in comparison with existing junction tree methods that also rely on materialization, our approach achieves competitive efficiency during inference using significantly lighter materialization.