Banister
发表于 2025-3-23 13:05:00
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coqgrams that (1) depend on some unknown code satisfying a specification or that (2) return objects conforming to a certain specification. All of our results have been formally verified in the interactive theorem prover Coq.
FLIC
发表于 2025-3-23 14:06:22
Relational Decompositionosition is applicable across heterogeneous pairs of transition systems. We apply our approach to justify variants of Benton’s Relational Hoare Logic (RHL) for a language with objects, and present novel rules for relating loops that fail to proceed in lockstep. We also outline applications to noninterference and separation logic.
防水
发表于 2025-3-23 18:03:43
Proving Valid Quantified Boolean Formulas in HOL Light’s outputs based on the LCF approach. An error in Squolem was discovered thanks to the integration. Experiments show that the feasibility of the integration is very sensitive to implementation of HOL Light and used inferences. This resulted in improvements in HOL Light’s inference system.
monogamy
发表于 2025-3-24 00:07:28
0302-9743 m rewriting, theorem proving, computability theory, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.978-3-642-22862-9978-3-642-22863-6Series ISSN 0302-9743 Series E-ISSN 1611-3349
赏钱
发表于 2025-3-24 04:00:01
http://reply.papertrans.cn/48/4706/470571/470571_15.png
NAIVE
发表于 2025-3-24 08:06:40
Towards Robustness Analysis Using PVSties under consideration here. In this paper, we briefly explain the shortcomings of ACL2 relatively to our problem, and we investigate the application of PVS, thus enabling to improve our simple and multiple faults models and the associated verification methodology.
exorbitant
发表于 2025-3-24 10:45:14
http://reply.papertrans.cn/48/4706/470571/470571_17.png
干旱
发表于 2025-3-24 18:22:03
Three Chapters of Measure Theory in Isabelle/HOL Fubini’s theorem. We define the Lebesgue measure using the gauge integral available in Isabelle’s multivariate analysis. Finally, we relate both integrals and equate the integral on Euclidean spaces with iterated integrals. This work covers most of the first three chapters of Bauer’s measure theory textbook.
催眠
发表于 2025-3-24 20:28:11
http://reply.papertrans.cn/48/4706/470571/470571_19.png
安定
发表于 2025-3-25 00:06:37
Animating the Formalised Semantics of a Java-Like Languageuch as the reflexive transitive closure and Russell’s definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind.