Titlebook: Computer Aided Verification; 27th International C Daniel Kroening,Corina S. Păsăreanu Conference proceedings 2015 Springer International Pu

Ensign

书目名称Computer Aided Verification影响因子(影响力)




书目名称Computer Aided Verification影响因子(影响力)学科排名




书目名称Computer Aided Verification网络公开度




书目名称Computer Aided Verification网络公开度学科排名




书目名称Computer Aided Verification被引频次




书目名称Computer Aided Verification被引频次学科排名




书目名称Computer Aided Verification年度引用




书目名称Computer Aided Verification年度引用学科排名




书目名称Computer Aided Verification读者反馈




书目名称Computer Aided Verification读者反馈学科排名

BRIDE

On Automation of CTL* Verification for Infinite-State Systemsd uses an internal encoding which facilitates reasoning about the subtle interplay between the nesting of path and state temporal operators that occurs within .. proofs. A precondition synthesis strategy is then used over a program transformation which trades nondeterminism in the transition relatio

不公开

Algorithms for Model Checking HyperLTL and HyperCTL, free fragments of HyperLTL and HyperCTL. the automaton construction allows us to leverage existing model checking technology. Along several case studies, we demonstrate that the approach enables the verification of real hardware designs for properties that could not be checked before. We study infor

gruelling

plasma-cells

揉杂

揉杂

Skipping Refinementefinement involves defining an abstract, high-level . system and a concrete, low-level . system. One then shows that every behavior allowed by the implementation is also allowed by the specification. Due to the difference in abstraction levels, it is often the case that the implementation requires m

intangibility

Percentile Queries in Multi-dimensional Markov Decision Processesuire the analysis of trade-offs. In this paper, we study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function ., thresholds . (one per dimension), and pr

LAY

Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth,

GOAD

Counterexample Explanation by Learning Small Strategies in Markov Decision Processesly more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinis