Titlebook: Correct System Design; Symposium in Honor o Roland Meyer,André Platzer,Heike Wehrheim Conference proceedings 2015 Springer International Pu

水平

书目名称Correct System Design影响因子(影响力)




书目名称Correct System Design影响因子(影响力)学科排名




书目名称Correct System Design网络公开度




书目名称Correct System Design网络公开度学科排名




书目名称Correct System Design被引频次




书目名称Correct System Design被引频次学科排名




书目名称Correct System Design年度引用




书目名称Correct System Design年度引用学科排名




书目名称Correct System Design读者反馈




书目名称Correct System Design读者反馈学科排名

傀儡

Automated Reasoning Building Blocksclause learning (CDCL) and superposition, respectively. In this paper I identify these building blocks by a projection of superposition to propositional logic. Underlying both calculi is a partial model assumption guiding ordered resolution inferences that are not redundant.

POINT

Being and Change: Reasoning About Invariancestatement is a predicate that describes that part of the state that can be changed by the statement. We define invariance of an assertion with respect to a foot-print by means of a logical operation. This new Hoare logic is applied in a new simpler and modular proof of correctness of the well-known Quicksort sorting algorithm.

动机

Brain-Waves

细胞

细胞

statement is a predicate that describes that part of the state that can be changed by the statement. We define invariance of an assertion with respect to a foot-print by means of a logical operation. This new Hoare logic is applied in a new simpler and modular proof of correctness of the well-known Quicksort sorting algorithm.

debacle

Shervin Shajiee,Lucy Y. Pao,Robert R. McLeodThe Festschrift and associated symposium celebrate Ernst-Rüdiger Olderog’s 60th birthday with invited contributions of colleagues, all touching the theme of formal modeling and correctness in system design. Here, we would like to say some words about Ernst-Rüdiger Olderog himself and his contributions to formal methods research over the years.

冷淡一切

Shervin Shajiee,Lucy Y. Pao,Robert R. McLeodWe present two views of probabilistic programs and their relationship. An operational interpretation as well as a weakest pre-condition semantics are provided for an elementary probabilistic guarded command language. Our study treats important features such as sampling, conditioning, loop divergence, and non-determinism.

远足

Protecting Against Sovereign Defaults,We study how applicative bisimilarity behaves when instantiated on a call-by-value probabilistic .-calculus, endowed with Plotkin’s parallel disjunction operator. We prove that congruence and coincidence with the corresponding context relation hold for both bisimilarity and similarity, the latter known to be impossible in sequential languages.