apropos
发表于 2025-3-28 17:44:05
http://reply.papertrans.cn/24/2334/233349/233349_41.png
滑动
发表于 2025-3-28 18:49:56
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkersrld safety-critical systems remains challenging in practice. Inspired by goals set out in prior work, we report on a large-scale case study that applies modern verification techniques to check safety properties of a radiotherapy system in current clinical use. Because of the diversity and complexity
我正派
发表于 2025-3-29 01:08:36
End-to-End Verification of , Processors with ISA-Formalere are two significant factors: scaling issues and return on investment. The . include the size of modern processor specifications, the size/complexity of processor designs, the size of design/verification teams and the (non)availability of enough formal verification experts. The . issues include t
惊奇
发表于 2025-3-29 03:06:02
A Practical Verification Framework for Preemptive OS Kernelscontextual refinement of their abstract specifications. It provides a specification language for defining the high-level abstract model of OS kernels, a program logic for refinement verification of concurrent kernel code with multi-level hardware interrupts, and automated tactics for developing mech
傻瓜
发表于 2025-3-29 07:49:17
http://reply.papertrans.cn/24/2334/233349/233349_45.png
发展
发表于 2025-3-29 15:05:22
The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approachuling policy of the platform, the inputs may arrive at the reducers in different order. The . of reducers asks if the output of a reducer is independent of the order of its inputs. Although the problem is undecidable in general, the MapReduce programs in practice are usually used for data analytics
不遵守
发表于 2025-3-29 19:16:37
Liveness of Randomised Parameterised Systems under Arbitrary Schedulerssuch systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. In this paper we consider liveness under arbitrary (including
flourish
发表于 2025-3-29 22:52:08
http://reply.papertrans.cn/24/2334/233349/233349_48.png
Anal-Canal
发表于 2025-3-30 03:29:35
Hitting Families of Schedules for Asynchronous Programsrformed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these events can result in a bug. The number of schedules to be explored can, in general, be exponential..Empirically, many bugs in concurrent programs have been observed to ha
碎石
发表于 2025-3-30 08:04:06
XSat: A Fast Floating-Point Satisfiability Solvert code. Solving floating-point constraints is challenging in part because floating-point semantics is difficult to specify or abstract. State-of-the-art SMT solvers still often run into difficulties when solving complex, non-linear floating-point constraints..This paper proposes a new approach to SM