Task VC: Veriﬁcation Support for Heterogeneous Processes
To develop veriﬁcation support for heterogeneous processes, we investigate techniques to decompose complex propositions into a combination of propositions in individual logics. Based on experience with HOL-CSP, CSP-PROVER and CSP-CASL, we develop hetero- geneous proof calculi that combine available proof calculi for the process description with available proof calculi for the logic used for data representation, and moreover provide support for new heterogeneous constructs including the heterogeneous abstraction views developed in Work Package RA. The key aspects here are to identify powerful tools which can handle propositions in speciﬁc logic fragments (e.g. model checkers such as FDR, Spin, Uppaal, SMT provers, or SAT checkers), and develop a methodology how to decompose propositions and compose results from these tools in a more general framework, building on previous work on combining model checking and theorem proving by techniques such as data independence.