Том 44, № 1 (2018)

Model-based testing of event systems can take advantage of considering abstractions rather than explicit models, for controlling their size. When abstracting still a test has to be a concrete connected and reachable event sequence. This paper presents a test generation method based on computing a reachable and connected under-approximation of the abstraction of an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicatebased abstraction. We propose an algorithmic method that instantiates each of the abstract transitions, and maintains for widening it a frontier of concretely reached states. We present heuristics to favour the instances connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. This concrete under-approximation ends up covering partially (at best totally) the reachable abstract transitions. The computed tests are paths of the under-approximation. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.

C++ was originally designed as a sequential programming language. For development of multithreaded applications, libraries, such as Pthreads, Windows threads, and Boost, are traditionally used. The C++11 standard introduced some basic concepts and means for developing parallel and concurrent programs, but the direct use of these low-level means requires high programming skills and significant efforts. The absence of high-level models of parallelism in C++ is somewhat compensated for by various parallel libraries and directive parallelization tools (such as OpenMP), as well as by language extensions supported by some compilers (Intel CilkPlus). Nevertheless, we still require more advanced means to express parallelism in programs at the level of language standard and language library. In this survey, we consider the means for parallel and concurrent programming that are included into the C++17 standard, as well as some capabilities that are to be expected in the future standards.

The first-order intuitionistic logic is a formal theory from the family of constructive logics. In intuitionistic logic, it is possible to extract a particular example x = a and a proof of a formula P(a) from a proof of a formula ∃xP(x). Owing to this feature, intuitionistic logic has many applications in mathematics and computer science. Many modern proof assistants include automated tactics for the first-order intuitionistic logic, which simplify the task of solving challenging problems, such as formal verification of software, hardware, and protocols. In this paper, a new theorem prover (called WhaleProver) for full first-order intuitionistic logic is presented. Testing on the ILTP benchmarking library has shown that WhaleProver performance is comparable with the state-of-the-art intuitionistic provers. Our prover has solved more than 800 problems from the ILTP version 1.1.2. Some of them are intractable for other provers. WhaleProver is based on the inverse method proposed by S.Yu. Maslov. We introduce an intuitionistic inverse method calculus which is, in turn, a special kind of sequent calculus. It is also described how to adopt for this calculus several existing proof search strategies proposed for different logical calculi by S.Yu. Maslov, V.P. Orevkov, A.A. Voronkov, and others. In addition, a new proof search strategy is proposed that allows one to avoid redundant inferences. The paper includes results of experiments with WhaleProver on the ILTP library. We believe that Whale- Prover can be used as a test bench for different inference procedures and strategies, as well as for educational purposes.