共查询到10条相似文献,搜索用时 109 毫秒
1.
We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase
automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock
synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in
Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive
Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch
[LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify
parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be
handled by automatic first-order provers with support for arithmetics. 相似文献
2.
Tobias Nipkow 《Formal Aspects of Computing》1998,10(2):171-186
We present a formalization of the first 100 pages of Winskel's textbook The Formal Semantics of Programming Languages in
the theorem prover Isabelle/HOL: 2 operational, 2 denotational, 2 axiomatic semantics, a verification condition generator,
and the necessary soundness, completeness and equivalence proofs, all for a simple imperative programming language.
Received March 1997 / Accepted in revised form June 1998 相似文献
3.
Bytecode subroutines are a major complication for Java bytecode verification: They are difficult to fit into the dataflow
analysis that the JVM specification suggests. Hence, subroutines are left out or are restricted in most formalizations of
the bytecode verifier. We examine the problems that occur with subroutines and give an overview of the most prominent solutions
in the literature. Using the theorem prover Isabelle/HOL, we have extended our substantial formalization of the JVM and the
bytecode verifier with its proof of correctness by the most general solution for bytecode subroutines.
This revised version was published online in August 2006 with corrections to the Cover Date. 相似文献
4.
Anders Schlichtkrull 《Journal of Automated Reasoning》2018,61(1-4):455-484
I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations and semantic trees. The correspondence between unsatisfiable sets of clauses and finite semantic trees is formalized in Herbrand’s theorem. I discuss the difficulties that I had formalizing proofs of the lifting lemma found in the literature, and I formalize a correct proof. The completeness proof is by induction on the size of a finite semantic tree. Throughout the paper I emphasize details that are often glossed over in paper proofs. I give a thorough overview of formalizations of first-order logic found in the literature. The formalization of resolution is part of the IsaFoL project, which is an effort to formalize logics in Isabelle/HOL. 相似文献
5.
Jasmin Christian Blanchette Sascha Böhme Mathias Fleury Steffen Juilf Smolka Albert Steckermeier 《Journal of Automated Reasoning》2016,56(2):155-200
Sledgehammer is a component of the Isabelle/HOL proof assistant that integrates external automatic theorem provers (ATPs) to discharge interactive proof obligations. As a safeguard against bugs, the proofs found by the external provers are reconstructed in Isabelle. Reconstructing complex arguments involves translating them to Isabelle’s Isar format, supplying suitable justifications for each step. Sledgehammer transforms the proofs by contradiction into direct proofs; it iteratively tests and compresses the output, resulting in simpler and faster proofs; and it supports a wide range of ATPs, including E, LEO-II, Satallax, SPASS, Vampire, veriT, Waldmeister, and Z3. 相似文献
6.
The real-time process calculus Timed CSP is capable of expressing properties such as deadlock-freedom and real-time constraints.
It is therefore well-suited to model and verify embedded software. However, proofs about Timed CSP specifications are not
ensured to be correct since comprehensive machine-assistance for Timed CSP is not yet available. In this paper, we present
our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic
semantics together with bisimulation equivalences and coalgebraic invariants. This allows for semi-automated and mechanically
checked proofs about Timed CSP specifications. Mechanically checked proofs enhance confidence in verification because corner
cases cannot be overlooked. We additionally apply our formalization to an abstract specification with real-time constraints.
This is the basis for our current work, in which we verify a simple real-time operating system deployed on a satellite. As
this operating system has to cope with arbitrarily many threads, we use verification techniques from the area of parameterized
systems for which we outline their formalization. 相似文献
7.
Jasmin Christian Blanchette Sascha Böhme Lawrence C. Paulson 《Journal of Automated Reasoning》2013,51(1):109-128
Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. The ATPs and SMT solvers nicely complement each other, and Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach. 相似文献
8.
Sascha Böhme Michał Moskal Wolfram Schulte Burkhart Wolff 《Journal of Automated Reasoning》2010,44(1-2):111-144
Boogie is a verification condition generator for an imperative core language. It has front-ends for the programming languages C# and C enriched by annotations in first-order logic, i.e. pre- and postconditions, assertions, and loop invariants. Moreover, concepts like ghost fields, ghost variables, ghost code and specification functions have been introduced to support a specific modeling methodology. Boogie’s verification conditions—constructed via a wp calculus from annotated programs—are usually transferred to automated theorem provers such as Simplify or Z3. This also comprises the expansion of language-specific modeling constructs in terms of a theory describing memory and elementary operations on it; this theory is called a machine/memory model. In this paper, we present a proof environment, HOL-Boogie, that combines Boogie with the interactive theorem prover Isabelle/HOL, for a specific C front-end and a machine/memory model. In particular, we present specific techniques combining automated and interactive proof methods for code verification. The main goal of our environment is to help program verification engineers in their task to “debug” annotations and to find combined proofs where purely automatic proof attempts fail. 相似文献
9.
We describe and verify an elegant equivalence checker for regular expressions. It works by constructing a bisimulation relation between (derivatives of) regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, composition and (reflexive) transitive closure is obtained. The verification is carried out in the theorem prover Isabelle/HOL, yielding a practically useful decision procedure. 相似文献
10.
Jan Olaf Blech Sabine Glesner Johannes Leitner Steffen Mülling 《Electronic Notes in Theoretical Computer Science》2005,141(2):33-49
Correctness of compilers is a vital precondition for the correctness of the software translated by them. In this paper, we present two approaches for the formalization of static single assignment (SSA) form together with two corresponding formal proofs in the Isabelle/HOL system, each showing the correctness of code generation. Our comparison between the two proofs shows that it is very important to find adequate formalizations in formal proofs since they can simplify the verification task considerably. Our formal correctness proofs do not only verify the correctness of a certain class of code generation algorithms but also give us sufficient, easily checkable correctness criteria characterizing correct compilation results obtained from implementations (compilers) of these algorithms. These correctness criteria can be used in a compiler result checker. 相似文献