<p>In this thesis an operational semantics for a subset of the Java Virtual Machine (JVM) is developed and presented. The subset contains standard operations such as control flow, computation, and memory management. In addition, the subset contains a treatment of parallel threads of execution.</p><p> </p><p>The operational semantics are embedded into a $µ$-calculus based proof assistant, called the VeriCode Proof Tool (VCPT). VCPT has been developed at the Swedish Institute of Computer Science (SICS), and has powerful features for proving inductive assertions.</p><p> </p><p>Some examples of proving properties of programs using the embedding are presented.</p> / <p>I det här examensarbetet presenteras en operationell semantik för en delmängd av Javas virtuella maskin. Den delmängd som hanteras innehåller kontrollflöde, beräkningar och minneshantering. Vidare beskrivs semantiken för parallella exekveringstrådar.</p><p>Den operationella semantiken formaliseras i en bevisassistent for $µ$-kalkyl, VeriCode Proof Tool (VCPT). VCPT har utvecklats vid Swedish Institiute of Computer Science (SICS), och har kraftfulla tekniker för att bevisa induktiva påståenden.</p><p>Några exempel på bevis av egenskaper hos program användandes formaliseringen presenteras också.</p>
| Identifer | oai:union.ndltd.org:UPSALLA/oai:DiVA.org:kth-9512 |
| Date | January 2005 |
| Creators | Lagerkvist, Mikael Zayenz |
| Publisher | KTH, Electronic, Computer and Software Systems, ECS |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, text |
| Relation | IMIT/LECS, ; 2005-70 |
Page generated in 0.0032 seconds