Library

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    Theorem proving in technology transfer: the user’s point of view (2000)
    Springer
    International journal on software tools for technology transfer 3 (2000), S. 1-12 
    Details
    ISSN: 1433-2787
    Keywords: Key words: Formal methods – Mechanized theorem proving
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. The aim of this paper is to discuss the potentials, problems and critical factors for the industrial usage of mechanized theorem proving. The approach followed in this paper is somehow unusual. The starting point is the results of an industrial project whose goal was the assessment of the state of the art of provers (and of tools supporting formal methods in general). We describe the project results in terms of evaluation criteria, classification of technologies and tools and critical factors for industrial take-up. We present the results of the assessment in the same spirit, the same kind of analysis and even the same terminology which were used in the presentations and in the deliverables of the project. This should result in a presentation of a “different view” of the problem of technology transfer in theorem proving, that we call the “user’s point of view”. In this way, we hope to give a new perspective in the discussion of the industrial take-up of the theorem proving technology.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/PL00010806
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    Mechanized result verification: an industrial application (2000)
    Springer
    International journal on software tools for technology transfer 3 (2000), S. 78-92 
    Details
    ISSN: 1433-2787
    Keywords: Key words: Mechanized result verification – Validation – Safety critical software – Decomposition – Online/offline checking
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. We present part of an industrial project where mechanized theorem proving is used for the validation of a translator which generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done “online”, at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some verification conditions; the other is done “offline”, once for all, interactively with a general purpose prover; the offline proof shows that the verification conditions checked by the online prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the online prover. This approach is called mechanized result verification. This paper describes the project requirements and explains the motivations to formal validation by mechanized result verification, provides an overview of the formalization of the specifications for the online prover and discusses in detail some issues we have addressed in the mechanized offline proof.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/PL00010809
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    Program tactics and logic tactics (1996)
    Springer
    Annals of mathematics and artificial intelligence 17 (1996), S. 235-259 
    Details
    ISSN: 1573-7470
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract In this paper we present a first order classical metatheory, called MT, with the following properties: (1) tactics are terms of the language of MT (we call these tactics,Logic Tactics); (2) there exists a mapping between Logic Tactics and the tactics developed as programs within the GETFOL theorem prover (we call these tactics,Program Tactics). MT is expressive enough to represent the most interesting tacticals, i.e.,then, orelse, try, progress andrepeat. repeat allows us to express Logic Tactics which correspond to Program Tactics which may not terminate. This work is part of a larger project which aims at the development and mechanization of a metatheory which can be used to reason about, extend and, possibly, modify the code implementing Program Tactics and the GETFOL basic inference rules.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF02127970
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Book
    Book
    Automated planning : theory and practice (2004)
    Amsterdam [u.a.] :Elsevier, Kaufmann,
    Details
    Title: Automated planning : theory and practice
    Author: Ghallab, Malik
    Contributer: Nau, Dana , Traverso, Paolo
    Edition: 1
    Publisher: Amsterdam [u.a.] :Elsevier, Kaufmann,
    Year of publication: 2004
    Pages: XXVIII, 635 S. : , Ill., graph. Darst.
    ISBN: 1-558-60856-7
    Type of Medium: Book
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    ZIB Catalog
    Zuse Institute Berlin get availability status
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...