ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

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
    Monograph available for loan
    Monograph available for loan
    LATEX : a document preparation system ; user's guide and reference manual ; [updated für LATEX 2E] (1994)
    Boston [u.a.] : Addison-Wesley
    Details Availability
    Call number: PIK M 034-02-0348
    Type of Medium: Monograph available for loan
    Pages: XVI, 272 S. , Ill., graph. Darst.
    Edition: 2. ed., 22. print
    ISBN: 0201529831
    Location: A 18 - must be ordered
    Branch Library: PIK Library
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    BOOK
    Link to Library Catalog
    get availability status
  • 2
    facet.materialart.
    Unknown
    TLA+: Whence, Wherefore, and Whither (2009)
    In:  CASI
    Details
    Publication Date: 2018-06-06
    Description: The evolution of my ideas on specification and verification, and how they led to the TLA+ specification language. What is good and bad about TLA+. A brief description of the next version of TLA+ and its tools. E.
    Keywords: Mathematical and Computer Sciences (General)
    Type: Proceedings of the First NASA Formal Methods Symposium; 3; NASA/CP-2009-215407
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 3
    Electronic Resource
    Electronic Resource
    A theorem on atomicity in distributed algorithms (1990)
    Springer
    Distributed computing 4 (1990), S. 59-68 
    Details
    ISSN: 1432-0452
    Keywords: Message passing ; Reduction
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Reasoning about a distributed algorithm is simplified if we can ignore the time needed to send and deliver messages and can instead pretend that a process sends a collection of messages as a single atomic action, with the messages delivered instantaneously as part of the action. A theorem is derived that proves the validity of such reasoning for a large class of algorithms. It generalizes and corrects a well-known folk theorem about when an operation in a multiprocess program can be considered atomic.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01786631
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    On interprocess communication (1986)
    Springer
    Distributed computing 1 (1986), S. 86-101 
    Details
    ISSN: 1432-0452
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Interprocess communication is studied without assuming any lower-level communication primitives. Three classes of communication registers are considered, and several constructions are given for implementing one class of register with a weaker class. The formalism developed in Part I is used in proving the correctness of these constructions.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01786228
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    Electronic Resource
    Electronic Resource
    On interprocess communication (1986)
    Springer
    Distributed computing 1 (1986), S. 77-85 
    Details
    ISSN: 1432-0452
    Keywords: Concurrent reading and writing ; Nonatomic operations ; Shared data
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A formalism for specifying and reasoning about concurrent systems is described. Unlike more conventional formalisms, it is not based upon atomic actions. A definition of what it means for one system to implement a higher-level system is given and justified. In Part II, the formalism is used to specify several classes of interprocess communication mechanisms and to prove the correctness of algorithms for implementing them.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01786227
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 6
    Electronic Resource
    Electronic Resource
    Critique of the Lake Arrowhead Three (1992)
    Springer
    Distributed computing 6 (1992), S. 65-71 
    Details
    ISSN: 1432-0452
    Keywords: Concurrency ; Serializability ; Specification ; Verification
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF02276641
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 7
    Electronic Resource
    Electronic Resource
    Lazy caching in TLA (1999)
    Springer
    Distributed computing 12 (1999), S. 151-174 
    Details
    ISSN: 1432-0452
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Summary. We address the problem, proposed by Gerth, of verifying that a simplified version of the lazy caching algorithm of Afek, Brown, and Merritt is sequentially consistent. We specify the algorithm and sequential consistency in TLA $^+$ , a formal specification language based on TLA (the Temporal Logic of Actions). We then describe how to construct and check a formal TLA correctness proof.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s004460050063
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 8
    Electronic Resource
    Electronic Resource
    Fairness and hyperfairness (2000)
    Springer
    Distributed computing 13 (2000), S. 239-245 
    Details
    ISSN: 1432-0452
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. The notion of fairness in trace-based formalisms is examined. It is argued that, in general, fairness means machine closure. The notion of hyperfairness introduced by Attie, Francez, and Grumberg is generalized to arbitrary action systems. Also examined are the fairness criteria proposed by Apt, Francez, and Katz.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/PL00008921
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 9
    Electronic Resource
    Electronic Resource
    How to write a long formula (1994)
    Springer
    Formal aspects of computing 6 (1994), S. 580-584 
    Details
    ISSN: 1433-299X
    Keywords: Mathematical notation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Standard mathematical notation works well for short formulas, but not for the longer ones often written by computer scientists. Notations are proposed to make one or two-page formulas easier to read and reason about.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01211870
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 10
    Electronic Resource
    Electronic Resource
    The ‘Hoare logic’ of concurrent programs (1980)
    Springer
    Acta informatica 14 (1980), S. 21-37 
    Details
    ISSN: 1432-0525
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Summary Hoare's logical system for specifying and proving partial correctness properties of sequential programs is generalized to concurrent programs. The basic idea is to define the assertion {P} S {Q} to mean that if execution is begun anywhere in S with P true, then P will remain true until S terminates, and Q will be true if and when S terminates. The predicates P and Q may depend upon program control locations as well as upon the values of variables. A system of inference rules and axiom schemas is given, and a formal correctness proof for a simple program is outlined. We show that by specifying certain requirements for the unimplemented parts, correctness properties can be proved without completely implementing the program. The relation to Pnueli's temporal logic formalism is also discussed.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00289062
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...