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
    Formal verification by symbolic evaluation of partially-ordered trajectories (1995)
    Springer
    Formal methods in system design 6 (1995), S. 147-189 
    Details
    ISSN: 1572-8102
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Symbolic trajectory evaluation provides a means to formally verify properties of a sequential system by a modified form of symbolic simulation. The desired system properties are expressed in a notation combining Boolean expressions and the temporal logic “next-time” operator. In its simplest form, each property is expressed as an assertion [A⇒C], where the antecedentA expresses some assumed conditions on the system state over a bounded time period, and the consequentC expresses conditions that should result. A generalization allows simple invariants to be established and proven automatically. The verifier operates on system models in which the state space is ordered by “information content”. By suitable restrictions to the specification notation, we guarantee that for every trajectory formula, there is a unique weakest state trajectory that satisfies it. Therefore, we can verify an assertion [A⇒C] by simulating the system over the weakest trajectory forA and testing adherence toC. Also, establishing invariants correspond to simple fixed point calculations. This paper presents the general theory underlying symbolic trajectory evaluation. It also illustrates the application of the theory to the taks of verifying switch-level circuits as well as more abstract implementations.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01383966
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Book
    Book
    Third Caltech Conference on very large scale Integration (1983)
    California :Computer Science Press,
    Details
    Title: Third Caltech Conference on very large scale Integration
    Author: Bryant, Randal
    Publisher: California :Computer Science Press,
    Year of publication: 1983
    Pages: 430 S.
    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
  • 3
    Book
    Book
    Computer systems : a programmer's perspective (2016)
    Boston, Mass. [u.a.] :Pearson,
    Details
    Title: Computer systems : a programmer's perspective
    Author: Bryant, Randal E.
    Contributer: O'Hallaron, David R.
    Edition: 3. ed., global ed.
    Publisher: Boston, Mass. [u.a.] :Pearson,
    Year of publication: 2016
    Pages: 1120 S. : , graph. Darst.
    Series Statement: Always learning
    ISBN: 978-1-292-10176-7 , 1-292-10176-8
    Type of Medium: Book
    Language: English
    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...