Automatic generation of random test inputs is an approach that can alleviate the challenges of manual test case design. However, random test cases may be ineffective in fault detection and increase testing cost, especially in systems where test execution is resource- and time-consuming. To remedy this, the domain knowledge of test engineers can be exploited to select potentially effective test cases. To this end, test selection constraints suggested by domain experts can be utilized either for filtering randomly generated test inputs or for direct generation of inputs using constraint solvers. In this article, we propose a domain specific language (DSL) for formalizing locality-based test selection constraints of autonomous agents and discuss the impact of test selection filters, specified in our DSL, on randomly generated test cases. We study and compare the performance of filtering and constraint solving approaches in generating selective test cases for different test scenario parameters and discuss the role of these parameters in test generation performance. Through our study, we provide criteria for suitability of the random data filtering approach versus the constraint solving one under the varying size and complexity of our testing problem. We formulate the corresponding research questions and answer them by designing and conducting experiments using QuickCheck for random test data generation with filtering and Z3 for constraint solving. Our observations and statistical analysis indicate that applying filters can significantly improve test efficiency of randomly generated test cases. Furthermore, we observe that test scenario parameters affect the performance of the filtering and constraint solving approaches differently. In particular, our results indicate that the two approaches have complementary strengths: random generation and filtering works best for large agent numbers and long paths, while its performance degrades in the larger grid sizes and more strict constraints. On the contrary, constraint solving has a robust performance for large grid sizes and strict constraints, while its performance degrades with more agents and long paths.

Autonomous vehicles (AVs) are crucial robotic systems that promise to improve our lives via safe, efficient, and inclusive transport–while posing some new challenges for the education of future researchers in the area, that our current research and education might not be ready to deal with: In particular, we don’t know what the AVs of the future will look like, practical learning is restricted due to cost and safety concerns, and a high degree of multidisciplinary knowledge is required. Here, following the broad outline of Active Student Participation theory, we propose a pedagogical approach targeted toward AVs called CAR that combines Creativity theory, Applied demo-oriented learning, and Real world research context. Furthermore, we report on applying the approach to stimulate learning and engagement in a master’s course, in which students freely created a demo with 10 small robots running ROS2 and Ubuntu on Raspberry Pis, in connection to an ongoing research project and a real current problem (SafeSmart and COVID-19). The results suggested the feasibility of the CAR approach for enabling learning, as well as mutual benefits for both the students and researchers involved, and indicated some possibilities for future improvement, toward more effective integration of research experiences into second cycle courses.

VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.

This paper is an experience report of team Halmstad from the participation in a competition organised by the i-GAME project, the Grand Cooperative Driving Challenge 2016. The competition was held in Helmond, The Netherlands, during the last weekend of May 2016. We give an overview of our car's control and communication system that was developed for the competition following the requirements and specifications of the i-GAME project. In particular, we describe our implementation of cooperative adaptive cruise control, our solution to the communication and logging requirements, as well as the high level decision making support. For the actual competition we did not manage to completely reach all of the goals set out by the organizers as well as ourselves. However, this did not prevent us from outperforming the competition. Moreover, the competition allowed us to collect data for further evaluation of our solutions to cooperative driving. Thus, we discuss what we believe were the strong points of our system, and discuss post-competition evaluation of the developments that were not fully integrated into our system during competition time.

Permission accounting is fundamental to modular, thread-local reasoning about concurrent programs. This paper presents a new, symbolic system for permission accounting. In existing systems, permissions are numeric value-based and refer to the current thread only. Our system is based on symbolic expressions that provide a view of permissions for all relevant threads in the scope of the permission originator - current thread or a lock. This enables: (a) better understanding of permission tracking for the specifier, (b) more natural specification of complex permission transfer scenarios, and (c) more efficient reasoning for verification tools (in particular, no reasoning about rational numbers is required). Our system is based on symbolic permission slicing to divide permissions between multiple owners, and on tracking the history of permission transfers by means of "I-owe-you" chains of permission owners. We acclimatised our permission system in the KeY verifier as well as in PVS, and proved correct with both tools a list of vital properties about our permissions. KeY is an interactive verification tool for Java and our primary target to employ our permission system. First results with the verification of concurrent Java programs using our permission system in KeY are also reported.

This paper discusses formal specification and verification of the synchronisation classes of the Java API. In many verification systems for concurrent programs, synchronisation is treated as a primitive operation. As a result, verification rules for synchronisation are hard-coded in the logic, and not verified. These rules describe the concrete semantics of the given synchronisation primitive, and manage how resources are protected by synchronisation. In contrast, this paper describes several synchronisation primitives at the specification level, by specifying the behaviour of synchronisation routines from the Java API at method level using permission-based Separation Logic. This gives a generalised, high-level, and easily extendable approach to formalisation of arbitrary synchronisation mechanisms, which allows for modular treatment of synchronisation in verification. Notably, our approach does not only apply to locks, but also to other synchronisation mechanisms such as semaphores and latches that we also discuss. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) implementations of all presented synchronisers, the paper discusses the verification of one of them.

This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1 , which is aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.