In this paper, aimed at dependently typed programmers, we present a novel connection between automated and interactive theorem proving paradigms. The novelty is that the connection offers a better trade-off between usability, efficiency and soundness when compared to existing techniques. This technique allows for a powerful interactive proof framework that facilitates efficient verification of finite domain theorems and guided construction of the proof of infinite domain theorems. Such situations typically occur with industrial verification. As a case study, an embedding of SAT and CTL model checking is presented, both of which have been implemented for the dependently typed proof assistant Agda.

Finally, an example of a real world railway control system is presented, and shown using our proof framework to be safe with respect to an abstract model of trains not colliding or derailing. We demonstrate how to formulate safety directly and show using interactive theorem proving that signalling principles imply safety. Therefore, a proof by an automated theorem prover that the signalling principles hold for a concrete system implies the overall safety. Therefore, instead of the need for domain experts to validate that the signalling principles imply safety they only need to make sure that the safety is formulated correctly. Therefore, some of the validation is replaced by verification using interactive theorem proving.

This paper formalizes the observable interface behaviour of open systems for a strongly-typed, concurrent object-oriented language with single-class inheritance. We formally characterize the observable behaviour in terms of interactions at the program-environment interface. The behaviour is given by transitions between contextual judgments, where the absent environment is represented abstractly as assumption context. A particular challenge is the fact that, when the system is considered as open, code from the environment can be inherited to the component and vice versa. This requires to incorporate an abstract version of the heap into the environment assumptions when characterizing the interface behaviour. We prove the soundness of the abstract interface description.

We consider models of CSP based on recording availability information, i.e. the models record what events could have been performed instead of those that were actually performed. We present many different varieties of such models. For each, we give a compositional semantics, congruent to the operational semantics, and prove full abstraction and no-junk results. We compare the expressiveness of the different models.

A well-known result by Palamidessi tells us that πmix (the π-calculus with mixed choice) is more expressive than πsep (its subset with only separate choice). The proof of this result analyses their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of ‘incestual’ processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this paper, we shed more light on this role by re-proving the above result – based on a proper formalization of what it means to break symmetries – without referring to another problem domain like leader election.

Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from πmix into πsep. We indicate how their proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential. Moreover, by abandoning the uniformity criterion, we show that there indeed is a reasonable encoding. We emphasize its underlying principle, which highlights the difference between breaking symmetries locally instead of globally.