Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
LICS
2012
IEEE
9 years 9 months ago
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
—Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This al...
Dmitriy Traytel, Andrei Popescu, Jasmin Christian ...
JACM
2002
163views more  JACM 2002»
11 years 6 months ago
Formal verification of standards for distance vector routing protocols
We show how to use an interactive theorem prover, HOL, together with a model checker, SPIN, to prove key properties of distance vector routing protocols. We do three case studies: ...
Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gu...
IWC
2000
106views more  IWC 2000»
11 years 6 months ago
An analysis of errors in interactive proof attempts
The practical utility of interactive, user-guided, theorem proving depends on the design of good interaction environments, the study of which should be grounded in methods of rese...
J. Stuart Aitken, Thomas F. Melham
ENTCS
2002
82views more  ENTCS 2002»
11 years 6 months ago
A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity
We give a short description of Hybrid, a new tool for interactive theorem proving, s introduced in [4]. It provides a form of Higher Order Abstract Syntax (HOAS) combined consiste...
Alberto Momigliano, Simon Ambler, Roy L. Crole
JUCS
2008
166views more  JUCS 2008»
11 years 6 months ago
ASM Refinement Preserving Invariants
: This paper gives a definition of ASM refinement suitable for the verification that a protocol implements atomic transactions. We used this definition as the basis of the formal v...
Gerhard Schellhorn
ENTCS
2008
90views more  ENTCS 2008»
11 years 6 months ago
Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic
The interactive theorem prover developed in the KeY project, which implements a sequent calculus for JavaCard Dynamic Logic (JavaCardDL) is based on taclets. Taclets are lightweig...
Richard Bubel, Andreas Roth, Philipp Rümmer
books