Titlebook: Interactive Theorem Proving; Second International Marko Eekelen,Herman Geuvers,Freek Wiedijk Conference proceedings 2011 Springer-Verlag Gm

Banister

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

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.

防水

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

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

赏钱

NAIVE

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

干旱

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.

催眠

安定

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.