古老
发表于 2025-3-30 10:26:43
An Improved Unrolling-Based Decision Procedure for Algebraic Data Types,this paper, we present a decision procedure for reasoning about data types using abstractions that are provided by .: fold functions that map instances of algebraic data types into values in a decidable domain. We show that the procedure is sound and complete for a class of . catamorphisms..Our work
不感兴趣
发表于 2025-3-30 14:35:05
http://reply.papertrans.cn/99/9818/981753/981753_52.png
树胶
发表于 2025-3-30 16:46:29
Verified Calculations,style, often employed on paper, in the context of mechanized reasoning, and in particular, program verification..This work leverages the power of SMT solvers to machine-check calculational proofs at the level of detail they are usually written by hand. It builds the support for calculations into the
Lethargic
发表于 2025-3-30 21:40:02
Preserving User Proofs across Specification Changes,oop invariant gets strengthened when additional properties are added to the specification. This causes all the related proof obligations to change; thus previous user verifications become invalid. Yet it is often the case that most of previous proof attempts (goal transformations, calls to interacti
强壮
发表于 2025-3-31 01:57:47
An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames,ation, which employs specifications in implicit dynamic frames. Recently, theoretical work has shown how the cores of these two verification logics can be formally related. However, the mechanisms for abstraction in the two tools are not obviously comparable; VeriFast employs parameterised recursive
深陷
发表于 2025-3-31 08:49:04
http://reply.papertrans.cn/99/9818/981753/981753_56.png
Noisome
发表于 2025-3-31 09:27:20
Verification of a Virtual Filesystem Switch,Linux. As all file systems in Linux, UBIFS implements the Virtual Filesystem Switch (VFS) interface. VFS in turn implements top-level POSIX operations. This paper bridges the gap between an abstract specification of POSIX and a realistic model of VFS by ASM refinement. The models and proofs are mech