Titlebook: Integrated Formal Methods; 14th International C Carlo A. Furia,Kirsten Winter Conference proceedings 2018 Springer Nature Switzerland AG 20

advocate

书目名称Integrated Formal Methods影响因子(影响力)




书目名称Integrated Formal Methods影响因子(影响力)学科排名




书目名称Integrated Formal Methods网络公开度




书目名称Integrated Formal Methods网络公开度学科排名




书目名称Integrated Formal Methods被引频次




书目名称Integrated Formal Methods被引频次学科排名




书目名称Integrated Formal Methods年度引用




书目名称Integrated Formal Methods年度引用学科排名




书目名称Integrated Formal Methods读者反馈




书目名称Integrated Formal Methods读者反馈学科排名

Indebted

A Precise Pictorial Language for Array Invariants,ransition graphs where preconditions, postconditions and invariants, rather than the program code, determine the main program structure. We demonstrate the approach with three examples, verified using the Why3 theorem prover frontend.

沙发

State-of-the-Art Model Checking for B and Event-B Using P,B and LTS,rtial order reduction and proper multi-core model checking are now available. The (improved) performance of this advanced tool link is benchmarked on a series of models with various sizes and compared to P.B.

合唱队

,Task Planning with OMT: An Application to Production Logistics,r we discuss our experience using Optimization Modulo Theories to synthesize . plans for multi-robot teams handling production processes within the RoboCup Logistics League. Besides presenting our results, we discuss challenges and possible directions for future development of OMT planning.

演讲

太空

联邦

动作谜

继而发生

,Making Linearizability Compositional for Partially Ordered Executions,d related models. Our method is an adaptation of simulation-based methods, but in contrast to other such methods, it does not require that the implementation totally orders its events. We apply our proof technique and show correctness of the Treiber stack that blocks on empty, annotated with C11 release-acquire synchronisation.

Distribution

Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA,er (i.e. the preorder of injective homomorphisms); we discuss the merits of each. Our main technical contributions are algorithms for building homomorphism-minimal models and for generating a set-of-support for the models of a theory, in each case by scripting interactions with an SMT solver.