Andere Kunden interessierten sich auch für
![A Document-Based Approach to Information and Business Process Modeling]( "A Document-Based Approach to Information and Business Process Modeling")
A Document-Based Approach to Information and Business Process Modeling32,99 €![Software Process Support]( "Software Process Support")
Software Process Support51,99 €![Goals Software Construction Process]( "Goals Software Construction Process")
Goals Software Construction Process38,99 €![A Grounded Theory of Software Process Model Adoption]( "A Grounded Theory of Software Process Model Adoption")
A Grounded Theory of Software Process Model Adoption38,99 €![Software Process Improvement]( "Software Process Improvement")
Software Process Improvement51,99 €![A Feedback Control Model for the Software Testing Process]( "A Feedback Control Model for the Software Testing Process")
A Feedback Control Model for the Software Testing Process44,99 €![Web Services-Based Composite Business Process Management]( "Web Services-Based Composite Business Process Management")
Web Services-Based Composite Business Process Management44,99 €
One of the major challenges in computer science is
to put programming on a firmer mathematical basis,
in order to improve the correctness of programs.
This book presents a semantic framework for
verifying safety properties of open sequential
programs. The presentation is focused on an Algol-
like language that embodies many of the core
ingredients of imperative and functional languages
and incorporates data abstraction in its syntax.
Game semantics is used to obtain a compositional,
incremental way of generating accurate models of
programs. Model-checking is made possible by giving
certain kinds of concrete automata-theoretic
representations of the model. A data-abstraction
refinement procedure is developed for model-checking
safety properties of programs with infinite integer
types. Abstraction refinement, assume-guarantee
reasoning and the L algorithm for learning regular
languages are combined to yield a procedure for
compositional verification. An implementation based
on the FDR model checker for the CSP process algebra
demonstrates practicality of the methods. The book
should be useful to researchers in the field of
Theory and Practice of Software.
to put programming on a firmer mathematical basis,
in order to improve the correctness of programs.
This book presents a semantic framework for
verifying safety properties of open sequential
programs. The presentation is focused on an Algol-
like language that embodies many of the core
ingredients of imperative and functional languages
and incorporates data abstraction in its syntax.
Game semantics is used to obtain a compositional,
incremental way of generating accurate models of
programs. Model-checking is made possible by giving
certain kinds of concrete automata-theoretic
representations of the model. A data-abstraction
refinement procedure is developed for model-checking
safety properties of programs with infinite integer
types. Abstraction refinement, assume-guarantee
reasoning and the L algorithm for learning regular
languages are combined to yield a procedure for
compositional verification. An implementation based
on the FDR model checker for the CSP process algebra
demonstrates practicality of the methods. The book
should be useful to researchers in the field of
Theory and Practice of Software.