## Models, Algebras and Logic of Engineering SoftwareThis volume focuses on the education of researchers, teachers, students and practitioners. As usual in engineering, a study and application of the relevant branches of mathematics is crucial both in education and practice. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Preface | 1 |

An Overview | 43 |

Unifying Theories of Parallel Programming | 81 |

Algorithmic and Deductive Verification Methods for CTL | 109 |

Exploiting Independence for Verification Refinement and Modularity | 195 |

On Translating Models and Properties | 209 |

Proving Theorems about Java and the JVM with ACL2 | 227 |

Assertions | 255 |

David Harel | 317 |

Micromodels of Software | 351 |

Modeling and Verifying a Lego Car Using Hybrid 10 Automata | 385 |

Author Index | 403 |

### Other editions - View all

### Common terms and phrases

abstraction actions algebra allows application approach assertion assume atoms basic behavior binding called checking complete components composition Computer concurrent condition cons consider construction contains correctness defined definition denote described engineering equal equational example execution expression fact field Figure formal formula function give given heap holds implementation induction initial instance interface introduce L2:List labels language List logic machine maps mathematical Maude means method module notation Note object operations path possible predicate present proof properties prove reduction reference refinement relation represented requirements result rewrite rules satisfies Science semantics sequence signature sort specification stack step structure symbols temporal theorem theory thread tool top-frame transition translation true unit variables verification