Models, Algebras and Logic of Engineering SoftwareManfred Broy, Markus Pizka This 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. |
Contents
Preface | 1 |
An Overview | 43 |
Unifying Theories of Parallel Programming | 81 |
Algorithmic and Deductive Verification Methods for CTL | 109 |
Software Specification and Verification in Rewriting Logic | 133 |
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 |
Capturing and Analyzing Reactive Behavior | 317 |
Micromodels of Software | 351 |
Modeling and Verifying a Lego Car Using Hybrid IO Automata | 385 |
Author Index | 403 |
Other editions - View all
Common terms and phrases
ACL2 algebra algorithm Alloy assertion atoms axioms basic behavior binary relation binding bytecode call stack components composed system composition Computer Science concurrent programs condition cons constraints construction declarative declarative programming defined definition defthm defun denote equational logic example execution expression finite formal function heap Hoare Hoare Logic Hoare triple implementation induction input int-fix Java Kripke structure L2:List labels List machine mathematical Maude method model checking module morphisms NeList notation object operand stack operations pop stack postcondition predicate programming language proof property refinement prove pushout reachable relation requirements result rev L2 rev V#0 rewrite theory rewriting logic rules satisfies semantics sequence sequential signature specification stack top-frame th step structure symbols system model temporal logic theorem thread tool transition transition relation translation tuple variables verification