Titlebook: Algebraic Methodology and Software Technology; 13th International C Michael Johnson,Dusko Pavlovic Conference proceedings 2011 The Editor(s

变更

书目名称Algebraic Methodology and Software Technology影响因子(影响力)




书目名称Algebraic Methodology and Software Technology影响因子(影响力)学科排名




书目名称Algebraic Methodology and Software Technology网络公开度




书目名称Algebraic Methodology and Software Technology网络公开度学科排名




书目名称Algebraic Methodology and Software Technology被引频次




书目名称Algebraic Methodology and Software Technology被引频次学科排名




书目名称Algebraic Methodology and Software Technology年度引用




书目名称Algebraic Methodology and Software Technology年度引用学科排名




书目名称Algebraic Methodology and Software Technology读者反馈




书目名称Algebraic Methodology and Software Technology读者反馈学科排名

非秘密

Verification of Common Interprocedural Compiler Optimizations Using Visibly Pushdown Kleene Algebra programming languages (sequences, alternatives, loops and code blocks) in a natural way. In this paper, this system is used to verify the following interprocedural compiler optimizations: interprocedural dead code elimination, inlining of functions, tail-recursion elimination, procedure reordering

水獭

现晕光

Model Refinement Using Bisimulation Quotientsuced into a smallish, finite bisimulation quotient. Second, the reduced system is refined in order to ensure a given property, using any known finite-state method. Third, the refined reduced system is expanded back into an adequate refinement of the system given initially. The proposed method is bas

宽容

采纳

Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programminggic programming supports recursive computations, and some logic programs resemble the inductive or coinductive definitions written in functional programming languages. In this paper, we give a coalgebraic semantics to logic programming. We show that ground logic programs can be modelled by either ..

Perigee

opprobrious

Matching Logic: An Alternative to Hoare/Floyd Logics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called .. Program configurations satisfy patterns iff they . their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use

刚毅

Program Calculation in Coqy. It requires human insights and creativity, and needs systems to help human to focus on clever parts of the derivation by automating tedious ones and verifying correctness of transformations. Different from many existing systems, we show in this paper that Coq, a popular theorem prover, provides a

我正派