標(biāo)題: Titlebook: Verified Software. Theories, Tools, and Experiments; 9th International Co Andrei Paskevich,Thomas Wies Conference proceedings 2017 Springer [打印本頁] 作者: cherub 時(shí)間: 2025-3-21 20:06
書目名稱Verified Software. Theories, Tools, and Experiments影響因子(影響力)
書目名稱Verified Software. Theories, Tools, and Experiments影響因子(影響力)學(xué)科排名
書目名稱Verified Software. Theories, Tools, and Experiments網(wǎng)絡(luò)公開度
書目名稱Verified Software. Theories, Tools, and Experiments網(wǎng)絡(luò)公開度學(xué)科排名
書目名稱Verified Software. Theories, Tools, and Experiments被引頻次
書目名稱Verified Software. Theories, Tools, and Experiments被引頻次學(xué)科排名
書目名稱Verified Software. Theories, Tools, and Experiments年度引用
書目名稱Verified Software. Theories, Tools, and Experiments年度引用學(xué)科排名
書目名稱Verified Software. Theories, Tools, and Experiments讀者反饋
書目名稱Verified Software. Theories, Tools, and Experiments讀者反饋學(xué)科排名
作者: Pigeon 時(shí)間: 2025-3-21 22:37
A Formal Analysis of the Compact Position Reporting Algorithm, being considered by the standards organizations, are formally proven to guarantee correct decoding under exact real arithmetic. In addition, this paper proposes mathematically equivalent, but computationally simpler forms to several expressions in the CPR functions in order to reduce imprecise calc作者: GLUE 時(shí)間: 2025-3-22 03:20
Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions, is spurious, the abstraction is refined until a correct inversion to the input hash target is produced. We show that the resultant system is faster for inverting the SHA-1 hash function than state-of-the-art inversion tools.作者: 把手 時(shí)間: 2025-3-22 06:28
An Abstraction Technique for Describing Concurrent Program Behaviour,ication examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool supp作者: Nuance 時(shí)間: 2025-3-22 10:48
Nicolas Jeannerod,Claude Marché,Ralf Treinenon of the future. Secondly, this volume is the first of an ESPRIT Basic Research Series of publications of research results. It is expected that the quality of content and broad distribution of this series will have a major impact in making the advances achieved accessible to the world of academic and industr978-3-642-76276-5978-3-642-76274-1作者: elucidate 時(shí)間: 2025-3-22 14:25 作者: Ceremony 時(shí)間: 2025-3-22 18:16 作者: 有效 時(shí)間: 2025-3-22 22:15
Rapha?l Rieu-Helft,Claude Marché,Guillaume Melquiond-time temporal logic ILT. (i.e., an integration of LTL and IL), a multi-agent infinitary epistemic linear-time temporal logic IELT. and a multi-agent epistemic bounded linear-time temporal logic ELT. are obtained as applications of the resulting embedding theorem and its extensions and modifications作者: Enteropathic 時(shí)間: 2025-3-23 02:55 作者: Osteoporosis 時(shí)間: 2025-3-23 07:22
Alexander Kogtenkov belief and everybody believes modalities (introducing marked modalities and indices) and special sequents serving as a termination criterion for non-derivability are introduced. For sequents containing positive occurrences of mutual belief modality sequents of special shape are used to specialize a作者: Panther 時(shí)間: 2025-3-23 13:18 作者: 預(yù)兆好 時(shí)間: 2025-3-23 17:50 作者: 使迷惑 時(shí)間: 2025-3-23 18:55 作者: 去掉 時(shí)間: 2025-3-23 23:56
provide an integer programming formulation of this novel problem which is capable of solving small-scale instances to proven optimality. In order to efficiently solve large-scale instances, we develop a metaheuristic algorithm. A computational study with instances generated from real-world data indi作者: Legion 時(shí)間: 2025-3-24 03:34 作者: Fortuitous 時(shí)間: 2025-3-24 07:53 作者: 障礙 時(shí)間: 2025-3-24 12:44
thors from 23 countries: Spain (23 authors), China (20), USA (16), Mexico (13), Japan (12), UK (11), Czech Republic (8), Korea and Sweden (7 each), Canada and I978-3-540-00532-2978-3-540-36456-6Series ISSN 0302-9743 Series E-ISSN 1611-3349 作者: 惡心 時(shí)間: 2025-3-24 18:41
Marc Schooldermannvironments, tools, and standards, and for linking together speci?cation and veri?cation of properties of individual agents and multi-agent systems. The CLIMA w978-3-540-88832-1978-3-540-88833-8Series ISSN 0302-9743 Series E-ISSN 1611-3349 作者: 頑固 時(shí)間: 2025-3-24 22:25 作者: STANT 時(shí)間: 2025-3-25 00:00 作者: 返老還童 時(shí)間: 2025-3-25 05:45 作者: 圖表證明 時(shí)間: 2025-3-25 11:05
Ran Chen,Jean-Jacques Lévyrators when agents have to process messages about a static world. We propose to consider agents’ belief state as a set of pairs 〈belief, origin of the belief〉 combined with a preference relation over the agents embedded in the multi-agent system. The belief revision procedure for handling received m作者: addition 時(shí)間: 2025-3-25 15:36 作者: Left-Atrium 時(shí)間: 2025-3-25 17:20
Rapha?l Rieu-Helft,Claude Marché,Guillaume Melquiondimportant logic for formalizing common knowledge reasoning. The research fields of both LTL and IL have independently been developed each other, and the relationship between them has not yet been discussed before. In this paper, the relationship between LTL and IL is clarified by showing an embeddin作者: Creditee 時(shí)間: 2025-3-25 22:26 作者: 放縱 時(shí)間: 2025-3-26 03:05 作者: Intact 時(shí)間: 2025-3-26 05:07 作者: 小爭吵 時(shí)間: 2025-3-26 11:56 作者: 離開可分裂 時(shí)間: 2025-3-26 15:05
Wytse Oortwijn,Stefan Blom,Dilian Gurov,Marieke Huisman,Marina Zaharieva-Stojanovskidal freight transportation system involves the use of different modes of transportation, such as trucks, trains, and ships, to move freight containers. However, this system is loaded with inefficiencies due to the poor availability of real-time coordination and disruptions, causing delays, increased作者: 推崇 時(shí)間: 2025-3-26 19:04 作者: 向下五度才偏 時(shí)間: 2025-3-27 00:59
Memory-Efficient Tactics for Randomized LTL Model Checking,execution time until a counterexample is found, but we demonstrate that the trade-off is biased in favor of our tactics. By applying our memory-efficient tactics to scalable models from the literature, we show that the increase in time is typically less than proportional to the saving in memory and may be exponentially smaller.作者: 移動(dòng) 時(shí)間: 2025-3-27 02:29 作者: 火海 時(shí)間: 2025-3-27 06:41 作者: 混合,攙雜 時(shí)間: 2025-3-27 10:44
,Proving JDK’s Dual Pivot Quicksort Correct,en for granted. De?Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit?(JDK) implementation of TimSort..We have formally analysed the other implementation of sorting in the JDK standard library: A highly efficient implementation of a dual pivot quic作者: GULLY 時(shí)間: 2025-3-27 17:31
A Semi-automatic Proof of Strong Connectivity,to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductive predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows the description of programs in a Why3-ML programming language (a 作者: Console 時(shí)間: 2025-3-27 20:20 作者: GULF 時(shí)間: 2025-3-27 23:11 作者: needle 時(shí)間: 2025-3-28 04:41
Automating the Verification of Floating-Point Programs, highly depends on the way the floating-point operations are interpreted in the logic supported by back-end provers. We address this challenge by combining multiple techniques to separately prove different parts of the desired properties. We use abstract interpretation to compute numerical bounds of作者: MILK 時(shí)間: 2025-3-28 07:45
Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions,ch is a SAT solver-based cryptanalysis tool for inverting hash functions. We reduce the . into the satisfiability problem for Boolean logic, and use . to construct preimages for these targets. . has two key features, namely, a multi-armed bandit based adaptive restart (MABR) policy and a counterexam作者: 無情 時(shí)間: 2025-3-28 10:47
Practical Void Safety, never null and possibly null references appears to be insufficient during object initialization when some fields declared as never null may be temporary null before the initialization completes. Unlike all previous publications on the subject, this work avoids explicit encoding of these intermediat作者: UNT 時(shí)間: 2025-3-28 18:26
Memory-Efficient Tactics for Randomized LTL Model Checking,etect accepting paths makes it feasible to check extremely large models, however a naive approach may encounter many non-accepting paths or require the storage of many explicit states, making it inefficient. We study here several alternative tactics that can often avoid these problems. Exploiting pr作者: 性行為放縱者 時(shí)間: 2025-3-28 19:54 作者: Negotiate 時(shí)間: 2025-3-29 01:00
An Abstraction Technique for Describing Concurrent Program Behaviour,iour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show t作者: 合唱隊(duì) 時(shí)間: 2025-3-29 05:15
Conference proceedings 2017 and Experiments, VSTTE 2017, held in Heidelberg, Germany, in July 2017..The 12 full papers?presented were carefully revised and selected from 20 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain 作者: 南極 時(shí)間: 2025-3-29 07:51
Conference proceedings 2017issions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies..作者: Keratectomy 時(shí)間: 2025-3-29 12:35
Verifying Branch-Free Assembly Code in Why3,can succeed using a high degree of automation in a short amount of time. Furthermore, our approach is sensitive to subtle memory aliasing issues, demonstrating that formal verification of security-critical assembly code is not only feasible, but also effective.
