標(biāo)題: Titlebook: Automated Technology for Verification and Analysis; 9th International Sy Tevfik Bultan,Pao-Ann Hsiung Conference proceedings 2011 Springer- [打印本頁(yè)] 作者: Coolidge 時(shí)間: 2025-3-21 18:49
書(shū)目名稱Automated Technology for Verification and Analysis影響因子(影響力)
書(shū)目名稱Automated Technology for Verification and Analysis影響因子(影響力)學(xué)科排名
書(shū)目名稱Automated Technology for Verification and Analysis網(wǎng)絡(luò)公開(kāi)度
書(shū)目名稱Automated Technology for Verification and Analysis網(wǎng)絡(luò)公開(kāi)度學(xué)科排名
書(shū)目名稱Automated Technology for Verification and Analysis被引頻次
書(shū)目名稱Automated Technology for Verification and Analysis被引頻次學(xué)科排名
書(shū)目名稱Automated Technology for Verification and Analysis年度引用
書(shū)目名稱Automated Technology for Verification and Analysis年度引用學(xué)科排名
書(shū)目名稱Automated Technology for Verification and Analysis讀者反饋
書(shū)目名稱Automated Technology for Verification and Analysis讀者反饋學(xué)科排名
作者: Dealing 時(shí)間: 2025-3-21 21:13 作者: 譏笑 時(shí)間: 2025-3-22 01:33
Zoltan J. Acs,László Szerb,Erkko Autions and the formal verification of some of their fundamental properties, such as Joint probabilities, Chapman-Kolmogorov equation and steady state probabilities, using the HOL theorem prover. For illustration purposes, we utilize our formalization to analyze a simplified binary communication channel.作者: lobster 時(shí)間: 2025-3-22 06:20 作者: 天空 時(shí)間: 2025-3-22 12:48 作者: Carcinogen 時(shí)間: 2025-3-22 14:49 作者: Minuet 時(shí)間: 2025-3-22 18:01
Nondeterministic Update of CTL Models by Preserving Satisfaction through Protectionson, our algorithm can efficiently generate a model to satisfy a specification of mutual exclusion in a variant of CTL. Such a variant extends CTL with an operator that limits the out-degree of states. We compare our method with a generate-and-test algorithm and outline a proof of soundness and completeness for our method.作者: 仲裁者 時(shí)間: 2025-3-22 22:32
Formalization of Finite-State Discrete-Time Markov Chains in HOLns and the formal verification of some of their fundamental properties, such as Joint probabilities, Chapman-Kolmogorov equation and steady state probabilities, using the HOL theorem prover. For illustration purposes, we utilize our formalization to analyze a simplified binary communication channel.作者: lactic 時(shí)間: 2025-3-23 03:26 作者: Affiliation 時(shí)間: 2025-3-23 08:43
Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking.作者: LITHE 時(shí)間: 2025-3-23 13:47
Won-Yong Oh,Kyoung Jin Choi,Young K. Changnt. We propose simple measures which we, as a community, could adopt to make the design of serious verification tools easier and more credible. Our long-term vision is for the community to produce tools that are indispensable for a developer but so seamlessly integrated into a development environment, as to be invisible.作者: 儀式 時(shí)間: 2025-3-23 14:08 作者: 命令變成大炮 時(shí)間: 2025-3-23 21:38 作者: Alopecia-Areata 時(shí)間: 2025-3-23 23:55 作者: 浪費(fèi)時(shí)間 時(shí)間: 2025-3-24 05:19 作者: BLINK 時(shí)間: 2025-3-24 08:53
Maria Ragland,Khairy M. Soliman we propose a hierarchical approach to the synthesis problem by solving it first for sub problems and using the results for state space reduction in the full problem. A secondary contribution concerns combined safety and liveness control objectives that approximate stabilization.作者: Obedient 時(shí)間: 2025-3-24 14:14 作者: 2否定 時(shí)間: 2025-3-24 17:02 作者: 路標(biāo) 時(shí)間: 2025-3-24 22:58 作者: 不知疲倦 時(shí)間: 2025-3-25 01:43
0302-9743 national Symposium on Automated Technology for Verification and Analysis, ATVA 2011, held in Taipei, Taiwan, in October 2011..The 23 revised regular papers presented together with 5 invited papers, 11 short papers, and 2 tool papers, were carefully reviewed and selected from 75 submissions. The pape作者: CRUDE 時(shí)間: 2025-3-25 03:36
Andreas Kornelakis,Horen Voskeritsianemical reactions in Systems Biology. The main problem with Statistical Model Checking is caused by rare events. We describe how Statistical Model Checking works and demonstrate the problem with rare events. We then describe how Importance Sampling with the Cross-Entropy Technique can be used to address this problem.作者: 空氣 時(shí)間: 2025-3-25 10:57
Zoltan J. Acs,László Szerb,Ainsley Lloydpermissiveness?of) a?most permissive winning strategy is in NP∩coNP. Along the way, we?provide a new study of mean-payoff?parity games. In?particular, we?give a new algorithm for solving these games, which beats all previously known algorithms for this problem.作者: libertine 時(shí)間: 2025-3-25 14:49 作者: Communicate 時(shí)間: 2025-3-25 17:09 作者: 最小 時(shí)間: 2025-3-25 21:59 作者: Fulminate 時(shí)間: 2025-3-26 03:28 作者: antecedence 時(shí)間: 2025-3-26 08:10
A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems we propose a hierarchical approach to the synthesis problem by solving it first for sub problems and using the results for state space reduction in the full problem. A secondary contribution concerns combined safety and liveness control objectives that approximate stabilization.作者: Communicate 時(shí)間: 2025-3-26 12:31
Modal Transition Systems: Composition and LTL Model Checking DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a?solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME.作者: ULCER 時(shí)間: 2025-3-26 16:21 作者: 1分開(kāi) 時(shí)間: 2025-3-26 20:38 作者: 狂怒 時(shí)間: 2025-3-26 21:18 作者: 殘忍 時(shí)間: 2025-3-27 02:05
An Alternative Definition for Timed Automata Compositionation of actions. Thereafter, we instantiate this framework for timed automata where we show how to associate such a TTS with two-levels static priority (committedness) to a TA and establish the compositionality theorem introduced by [5] with the mentioned refinement property.作者: Semblance 時(shí)間: 2025-3-27 08:31 作者: 美色花錢(qián) 時(shí)間: 2025-3-27 11:23
Formal Analysis of Online Algorithms. The first two contributions broaden the scope of our approach to settings in which the traditional analysis of online algorithms is particularly complicated. The third contribution improves the practicality of our approach and enables it to handle larger state spaces.作者: dowagers-hump 時(shí)間: 2025-3-27 15:05
Pawe? B?aszczyk,Tomasz B?aszczykWe introduce and study alternating weighted automata on finite words in both the max and sum semantics. We study the duality between the min and max semantics, closure under max and sum, the added power of universality and alternation, and arithmetic operations on automata. In particular, we show th作者: AGATE 時(shí)間: 2025-3-27 21:30 作者: ETCH 時(shí)間: 2025-3-28 00:09 作者: BABY 時(shí)間: 2025-3-28 03:39 作者: 嘴唇可修剪 時(shí)間: 2025-3-28 06:47 作者: 符合國(guó)情 時(shí)間: 2025-3-28 10:24
Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocolson and Jeffrey’s type system and develop a type inference algorithm for it, so that protocols can be verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier S.CA2 based on the algorithm, and confirmed its effectiveness.作者: 詩(shī)集 時(shí)間: 2025-3-28 16:39
Model Checking EGF on Basic Parallel Processesic EF with the CTL* notation EGF, which means that there exists an infinite path on which there are infinitely many entries satisfying certain property. We prove that this problem is PSPACE-complete, and .-complete for certain classes of fixed formula with the nesting depth . of modal operators.作者: Oversee 時(shí)間: 2025-3-28 19:24
Tevfik Bultan,Pao-Ann HsiungFast track conference proceedings.Unique visibility.State of the art research作者: OTTER 時(shí)間: 2025-3-28 23:50
Lecture Notes in Computer Sciencehttp://image.papertrans.cn/b/image/166361.jpg作者: sterilization 時(shí)間: 2025-3-29 03:16 作者: 離開(kāi)真充足 時(shí)間: 2025-3-29 09:09
Zoltan J. Acs,László Szerb,Erkko Autioon and Jeffrey’s type system and develop a type inference algorithm for it, so that protocols can be verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier S.CA2 based on the algorithm, and confirmed its effectiveness.作者: ungainly 時(shí)間: 2025-3-29 15:24
Zoltan J. Acs,László Szerb,Ainsley Lloydic EF with the CTL* notation EGF, which means that there exists an infinite path on which there are infinitely many entries satisfying certain property. We prove that this problem is PSPACE-complete, and .-complete for certain classes of fixed formula with the nesting depth . of modal operators.作者: Fillet,Filet 時(shí)間: 2025-3-29 18:20 作者: 阻擋 時(shí)間: 2025-3-29 20:39 作者: 車床 時(shí)間: 2025-3-30 02:43 作者: abreast 時(shí)間: 2025-3-30 06:35 作者: diabetes 時(shí)間: 2025-3-30 10:29 作者: 冰雹 時(shí)間: 2025-3-30 15:40
https://doi.org/10.1057/9781137510709ocols are basically collections of individual transactions or commands, such as simple read/write and bust read/write, and each transaction or command can be specified with a FSM. So a given communication protocol can be represented with a set of FSMs which work jointly. Based on these FSM-based spe作者: 同位素 時(shí)間: 2025-3-30 18:39 作者: Hangar 時(shí)間: 2025-3-30 21:04
Zoltan J. Acs,László Szerb,Erkko Autioel update face a difficulty: deleting (adding) transitions from (to) a Kripke model to satisfy a universal (an existential) subformula may dissatisfy some existential (universal) subformulas. Our method employs protected models to overcome this difficulty. We demonstrate our algorithm with a classic作者: 事物的方面 時(shí)間: 2025-3-31 03:47
Zoltan J. Acs,László Szerb,Erkko Autioon and Jeffrey’s type system and develop a type inference algorithm for it, so that protocols can be verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier S.CA2 based on the algorithm, and confirmed its effectiveness.作者: 頂點(diǎn) 時(shí)間: 2025-3-31 05:36
Zoltan J. Acs,László Szerb,Erkko Autionalyzed using computer simulation, and more recently using probabilistic model-checking but these methods either do not guarantee accurate analysis or are not scalable. As an alternative, we propose to use higher-order-logic theorem proving to reason about properties of systems that can be described作者: 皺痕 時(shí)間: 2025-3-31 11:33 作者: ensemble 時(shí)間: 2025-3-31 13:30 作者: 一美元 時(shí)間: 2025-3-31 18:31
Zoltan J. Acs,László Szerb,Ainsley Lloyd in terms of the . number/weight of transitions blocked by a?strategy. Using a translation into mean-payoff parity games, we?prove that deciding (the permissiveness?of) a?most permissive winning strategy is in NP∩coNP. Along the way, we?provide a new study of mean-payoff?parity games. In?particular,作者: 阻擋 時(shí)間: 2025-3-31 23:20
Zoltán J.‘ács,László Szerb,Ainsley Lloydn enabled actions. Our core method combines the concept of fault- localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce co作者: arrogant 時(shí)間: 2025-4-1 02:48 作者: Encoding 時(shí)間: 2025-4-1 08:39 作者: osteoclasts 時(shí)間: 2025-4-1 12:13
Maria Ragland,Khairy M. Solimanstates are grouped together in a finite index partition at the price of a non-deterministic over approximation of the transition relation. The main contribution of this work is a technique to reduce the state explosion generated by the discretization: exploiting structural properties of ODE systems,
