主动
发表于 2025-3-25 06:13:48
http://reply.papertrans.cn/48/4762/476177/476177_21.png
使入迷
发表于 2025-3-25 08:10:21
http://reply.papertrans.cn/48/4762/476177/476177_22.png
Acupressure
发表于 2025-3-25 15:44:50
Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Studyssion algorithm that aims to be simple, have a good compression ratio and be fast to execute. We present the choices we make in the implementation and the specification, which enable the verification effort.
有恶臭
发表于 2025-3-25 16:40:01
http://reply.papertrans.cn/48/4762/476177/476177_24.png
松果
发表于 2025-3-25 23:53:28
Proving Termination via Measure Transfer in Equivalence Checkingose derived from definitions of functions. For such inductive proofs to be sound, it is necessary to establish that the functions terminate, which is a challenging problem on its own. In this paper, we consider termination in the context of equivalence checking of a candidate program against a prova
运动性
发表于 2025-3-26 03:22:53
PLACIDUS: Engineering Product Lines of Rigorous Assurance Casesy evidence artifacts (e.g., test results, proofs). ACs can also be studied as formal objects in themselves, such that formal methods can be used to establish their correctness. Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), wherein a family of rela
extemporaneous
发表于 2025-3-26 08:20:25
Stateful Functional Modeling with Refinement (a Lean4 Framework)rt a step-wise refinement methodology inspired by the Event-B formal method. The implementation provides the main Event-B constructions such as contexts, machines, events and, most importantly, the associated refinement principles. We also experiment with extensions such as event combinators and fun
arboretum
发表于 2025-3-26 11:31:03
Modeling Register Pairs in CompCerta machine-checkable correctness proof. We introduce CompCert., an extension of the CompCert compiler, which incorporates the modeling of register pairs. This enhancement targets 32-bit architectures, such as the 32-bit Arm, which combine two registers to support 64-bit operands. So far, CompCert abs
大门在汇总
发表于 2025-3-26 13:12:25
Monitoring Extended Hypernode Logicirst, we split the stutter-reduced prefix predicate into an explicit stutter-reduction operator and the classical prefix predicate on words. This change gives hypernode logic the ability to combine synchronous and asynchronous reasoning by explicitly stating which parts of traces can stutter. Second
全部
发表于 2025-3-26 18:31:42
http://reply.papertrans.cn/48/4762/476177/476177_30.png