抱狗不敢前
发表于 2025-3-26 23:42:13
http://reply.papertrans.cn/47/4686/468516/468516_31.png
会犯错误
发表于 2025-3-27 04:30:01
http://reply.papertrans.cn/47/4686/468516/468516_32.png
帽子
发表于 2025-3-27 07:11:48
An Event-B Based Generic Framework for Hybrid Systems Formal Modellingof heavy mathematical features, and related proofs. This paper presents a generic and reusable framework with different patterns, aimed at easing the design and verification of hybrid systems. It relies on refinement and proofs using Event-B, and defines an easily extensible set of generic patterns
Ovulation
发表于 2025-3-27 12:23:54
Towards Generating SPARK from Event-B Modelsf annotations. Properties of the Event-B models such as axioms and invariants are also translated and embedded in the resulting models as pre- and post-conditions. This helps with generating SPARK proof annotations automatically hence ensuring the correct behaviour of the resulting code. A prototype
倾听
发表于 2025-3-27 17:29:33
Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Jates user-defined taint analyses that are formally specified in a domain-specific language for expressing taint-flow analyses. We demonstrate how dynamic taint analysis can be integrated into ., a dynamic symbolic execution engine for the . virtual machine in . PathFinder. The integration of the two
glacial
发表于 2025-3-27 21:13:43
Automatic Generation of Guard-Stable Floating-Point Codethmetic. This phenomenon is caused by the presence of round-off errors in floating-point computations. Writing programs that correctly handle guard instability often requires expertise on finite precision arithmetic. This paper presents a fully automatic toolchain that generates and formally verifie
Interregnum
发表于 2025-3-27 21:56:49
Formal Methods for GPGPU Programming: Is the Demand Met?rmine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of pro
Amenable
发表于 2025-3-28 02:45:47
http://reply.papertrans.cn/47/4686/468516/468516_38.png
justify
发表于 2025-3-28 08:42:44
History-Based Specification and Verification of Java Collections in KeYerface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations including their parameters and return value, on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a
简略
发表于 2025-3-28 10:43:35
http://reply.papertrans.cn/47/4686/468516/468516_40.png